File tree Expand file tree Collapse file tree 1 file changed +9
-0
lines changed
src/goto-instrument/contracts Expand file tree Collapse file tree 1 file changed +9
-0
lines changed Original file line number Diff line number Diff line change @@ -86,6 +86,15 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
8686 instructions.add (goto_programt::make_decl (lower_bound_address_var, location));
8787 instructions.add (goto_programt::make_decl (upper_bound_address_var, location));
8888
89+ instructions.add (goto_programt::make_assignment (
90+ lower_bound_address_var,
91+ null_pointer_exprt{to_pointer_type (slice.first .type ())},
92+ location));
93+ instructions.add (goto_programt::make_assignment (
94+ upper_bound_address_var,
95+ null_pointer_exprt{to_pointer_type (slice.first .type ())},
96+ location));
97+
8998 goto_programt skip_program;
9099 const auto skip_target = skip_program.add (goto_programt::make_skip (location));
91100
You can’t perform that action at this time.
0 commit comments