diff --git a/regression/cbmc/Quantifiers-statement-expression1/main.c b/regression/cbmc/Quantifiers-statement-expression1/main.c new file mode 100644 index 00000000000..a940665bd59 --- /dev/null +++ b/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; +} diff --git a/regression/cbmc/Quantifiers-statement-expression1/test.desc b/regression/cbmc/Quantifiers-statement-expression1/test.desc new file mode 100644 index 00000000000..9bab40c8f03 --- /dev/null +++ b/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 diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 4a605141902..5e49ce90f98 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/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); }