Skip to content

Commit a11060c

Browse files
committed
Fix side_effect_expr_nondett construction
Signed-off-by: František Nečas <[email protected]>
1 parent db122d7 commit a11060c

File tree

1 file changed

+5
-3
lines changed

1 file changed

+5
-3
lines changed

src/2ls/preprocessing_util.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,9 @@ void twols_parse_optionst::nondet_locals(goto_modelt &goto_model)
8484
to_symbol_expr(to_code_assign(next->code).lhs())==decl.symbol())
8585
continue;
8686

87-
side_effect_expr_nondett nondet(decl.symbol().type());
87+
side_effect_expr_nondett nondet(
88+
decl.symbol().type(),
89+
i_it->source_location);
8890
goto_programt::targett t=f_it->second.body.insert_after(i_it);
8991
t->make_assignment();
9092
code_assignt c(decl.symbol(), nondet);
@@ -747,10 +749,10 @@ void make_freed_ptr_comparison_nondet(
747749
and_exprt(
748750
or_exprt(
749751
lhs_not_freed_cond,
750-
side_effect_expr_nondett(bool_typet())),
752+
side_effect_expr_nondett(bool_typet(), loc->source_location)),
751753
or_exprt(
752754
rhs_not_freed_cond,
753-
side_effect_expr_nondett(bool_typet()))));
755+
side_effect_expr_nondett(bool_typet(), loc->source_location))));
754756
}
755757
}
756758
else if(cond.id()==ID_not)

0 commit comments

Comments
 (0)