Merge pull request #8649 from tautschnig/fix-quantifier-conversion

Fix statement-expression expansion for Kani-provided quantifiers

Author: remi-delmas-3000

regression/cbmc/Quantifiers-statement-expression1/main.c

@@ -0,0 +1,21 @@
+int main()
+{
+  __CPROVER_assert(
+    __CPROVER_forall {
+      int i;
+      ({
+        goto out;
+        i == i;
+      })
+    },
+    "");
+  __CPROVER_assert(
+    __CPROVER_forall {
+      int i;
+      ({ i == i; })
+    },
+    "");
+out:
+
+  return 0;
+}

regression/cbmc/Quantifiers-statement-expression1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+goto label 'out' not found
+^EXIT=6$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/goto-conversion/goto_clean_expr.cpp

@@ -61,9 +61,11 @@ static exprt convert_statement_expression(
   const quantifier_exprt &qex,
   const code_expressiont &code,
   const irep_idt &mode,
-  goto_convertt &converter)
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
 {
   goto_programt where;
+  goto_convertt converter{symbol_table, message_handler};
   converter.goto_convert(code, where, mode);
   where.compute_location_numbers();
 
@@ -716,7 +718,8 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
       code.operands()[0].get_named_sub()[ID_statement].id() ==
         ID_statement_expression)
     {
-      auto res = convert_statement_expression(qex, code, mode, *this);
+      auto res = convert_statement_expression(
+        qex, code, mode, symbol_table, get_message_handler());
       qex.where() = res;
       return clean_expr(res, mode, result_is_used);
     }