Skip to content

Commit 60d683f

Browse files
committed
Fix initialization of invalid CARs
1 parent 01505ec commit 60d683f

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/goto-instrument/contracts/assigns.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff 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

0 commit comments

Comments
 (0)