Skip to content

Commit 98f0035

Browse files
committed
Fix statement-expression expansion for Kani-provided quantifiers
CBMC side of model-checking/kani#4020: re-using the same converter instance would confuse finish-gotos (when really we don't want gotos inside the statement expression to be considered at all by the main goto-converter instances).
1 parent f1faa61 commit 98f0035

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,9 +61,11 @@ static exprt convert_statement_expression(
6161
const quantifier_exprt &qex,
6262
const code_expressiont &code,
6363
const irep_idt &mode,
64-
goto_convertt &converter)
64+
symbol_table_baset &symbol_table,
65+
message_handlert &message_handler)
6566
{
6667
goto_programt where;
68+
goto_convertt converter{symbol_table, message_handler};
6769
converter.goto_convert(code, where, mode);
6870
where.compute_location_numbers();
6971

@@ -716,7 +718,8 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
716718
code.operands()[0].get_named_sub()[ID_statement].id() ==
717719
ID_statement_expression)
718720
{
719-
auto res = convert_statement_expression(qex, code, mode, *this);
721+
auto res = convert_statement_expression(
722+
qex, code, mode, symbol_table, get_message_handler());
720723
qex.where() = res;
721724
return clean_expr(res, mode, result_is_used);
722725
}

0 commit comments

Comments
 (0)