@@ -1128,9 +1128,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
1128
1128
return true ;
1129
1129
}
1130
1130
1131
- auto &goto_program = function_obj->second .body ;
1131
+ auto &function_body = function_obj->second .body ;
1132
1132
1133
- if (check_for_looped_mallocs (goto_program ))
1133
+ if (check_for_looped_mallocs (function_body ))
1134
1134
{
1135
1135
return true ;
1136
1136
}
@@ -1144,22 +1144,22 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
1144
1144
function,
1145
1145
symbol_table);
1146
1146
1147
- // detect and add static local variables
1147
+ // Detect and add static local variables
1148
1148
assigns.add_static_locals_to_write_set (goto_functions, function);
1149
1149
1150
1150
// Add formal parameters to write set
1151
1151
for (const auto ¶m : to_code_type (target.type ).parameters ())
1152
1152
assigns.add_to_write_set (ns.lookup (param.get_identifier ()).symbol_expr ());
1153
1153
1154
- auto instruction_it = goto_program .instructions .begin ();
1154
+ auto instruction_it = function_body .instructions .begin ();
1155
1155
for (const auto &car : assigns.get_write_set ())
1156
1156
{
1157
1157
auto snapshot_instructions = car.generate_snapshot_instructions ();
1158
1158
insert_before_swap_and_advance (
1159
- goto_program , instruction_it, snapshot_instructions);
1159
+ function_body , instruction_it, snapshot_instructions);
1160
1160
};
1161
1161
1162
- // restore internal coherence in the programs
1162
+ // Restore internal coherence in the programs
1163
1163
goto_functions.update ();
1164
1164
1165
1165
// Full inlining of the function body
@@ -1173,23 +1173,23 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
1173
1173
decorated.get_recursive_function_warnings_count () == 0 ,
1174
1174
" Recursive functions found during inlining" );
1175
1175
1176
- // clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1177
- simplify_gotos (goto_program , ns);
1176
+ // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1177
+ simplify_gotos (function_body , ns);
1178
1178
1179
- // restore internal coherence in the programs
1179
+ // Restore internal coherence in the programs
1180
1180
goto_functions.update ();
1181
1181
1182
1182
INVARIANT (
1183
- is_loop_free (goto_program , ns, log),
1183
+ is_loop_free (function_body , ns, log),
1184
1184
" Loops remain in function '" + id2string (function) +
1185
1185
" ', assigns clause checking instrumentation cannot be applied." );
1186
1186
1187
1187
// Insert write set inclusion checks.
1188
1188
check_frame_conditions (
1189
- function_obj-> first ,
1190
- function_obj-> second . body ,
1189
+ function ,
1190
+ function_body ,
1191
1191
instruction_it,
1192
- function_obj-> second . body .instructions .end (),
1192
+ function_body .instructions .end (),
1193
1193
assigns,
1194
1194
// skip checks on function parameter assignments
1195
1195
true );
0 commit comments