@@ -134,7 +134,7 @@ class code_contractst
134
134
135
135
// / Inserts an assertion into the goto program to ensure that
136
136
// / an expression is within the assignable memory frame.
137
- void add_containment_check (
137
+ void add_inclusion_check (
138
138
goto_programt &,
139
139
const assigns_clauset &,
140
140
goto_programt::instructionst::iterator &,
@@ -144,19 +144,17 @@ class code_contractst
144
144
// / a goto statement that jumps back.
145
145
bool check_for_looped_mallocs (const goto_programt &program);
146
146
147
- // / Inserts an assertion statement into program before the assignment
147
+ // / Inserts an assertion into program immediately before the assignment
148
148
// / instruction_it, to ensure that the left-hand-side of the assignment
149
- // / aliases some expression in original_references, unless it is contained
150
- // / in freely assignable set.
149
+ // / is "included" in the (conditional address ranges in the) write set.
151
150
void instrument_assign_statement (
152
151
goto_programt::instructionst::iterator &,
153
152
goto_programt &,
154
153
assigns_clauset &);
155
154
156
- // / Inserts an assertion statement into program before the function call at
157
- // / ins_it, to ensure that any memory which may be written by the call is
158
- // / aliased by some expression in assigns_references, unless it is contained
159
- // / in freely assignable set.
155
+ // / Inserts an assertion into program immediately before the function call at
156
+ // / instruction_it, to ensure that all memory locations written to by the
157
+ // callee are "included" in the (conditional address ranges in the) write set.
160
158
void instrument_call_statement (
161
159
goto_programt::instructionst::iterator &,
162
160
const irep_idt &,
0 commit comments