@@ -165,66 +165,64 @@ bool jdiff_parse_optionst::process_goto_program(
165
165
const optionst &options,
166
166
goto_modelt &goto_model)
167
167
{
168
+ // remove function pointers
169
+ log .status () << " Removing function pointers and virtual functions"
170
+ << messaget::eom;
171
+ remove_function_pointers (
172
+ ui_message_handler, goto_model, cmdline.isset (" pointer-check" ));
173
+
174
+ // Java virtual functions -> explicit dispatch tables:
175
+ remove_virtual_functions (goto_model);
176
+
177
+ // remove Java throw and catch
178
+ // This introduces instanceof, so order is important:
179
+ remove_exceptions_using_instanceof (goto_model, ui_message_handler);
180
+
181
+ // Java instanceof -> clsid comparison:
182
+ class_hierarchyt class_hierarchy (goto_model.symbol_table );
183
+ remove_instanceof (goto_model, class_hierarchy, ui_message_handler);
184
+
185
+ mm_io (goto_model);
186
+
187
+ // instrument library preconditions
188
+ instrument_preconditions (goto_model);
189
+
190
+ // remove returns
191
+ remove_returns (goto_model);
192
+
193
+ // add generic checks
194
+ log .status () << " Generic Property Instrumentation" << messaget::eom;
195
+ goto_check_java (options, goto_model, ui_message_handler);
196
+
197
+ // checks don't know about adjusted float expressions
198
+ adjust_float_expressions (goto_model);
199
+
200
+ // recalculate numbers, etc.
201
+ goto_model.goto_functions .update ();
202
+
203
+ // instrument cover goals
204
+ if (cmdline.isset (" cover" ))
168
205
{
169
- // remove function pointers
170
- log .status () << " Removing function pointers and virtual functions"
171
- << messaget::eom;
172
- remove_function_pointers (
173
- ui_message_handler, goto_model, cmdline.isset (" pointer-check" ));
174
-
175
- // Java virtual functions -> explicit dispatch tables:
176
- remove_virtual_functions (goto_model);
177
-
178
- // remove Java throw and catch
179
- // This introduces instanceof, so order is important:
180
- remove_exceptions_using_instanceof (goto_model, ui_message_handler);
181
-
182
- // Java instanceof -> clsid comparison:
183
- class_hierarchyt class_hierarchy (goto_model.symbol_table );
184
- remove_instanceof (goto_model, class_hierarchy, ui_message_handler);
185
-
186
- mm_io (goto_model);
187
-
188
- // instrument library preconditions
189
- instrument_preconditions (goto_model);
190
-
191
- // remove returns
192
- remove_returns (goto_model);
193
-
194
- // add generic checks
195
- log .status () << " Generic Property Instrumentation" << messaget::eom;
196
- goto_check_java (options, goto_model, ui_message_handler);
197
-
198
- // checks don't know about adjusted float expressions
199
- adjust_float_expressions (goto_model);
200
-
201
- // recalculate numbers, etc.
202
- goto_model.goto_functions .update ();
203
-
204
- // instrument cover goals
205
- if (cmdline.isset (" cover" ))
206
- {
207
- // remove skips such that trivial GOTOs are deleted and not considered for
208
- // coverage annotation:
209
- remove_skip (goto_model);
210
-
211
- const auto cover_config =
212
- get_cover_config (options, goto_model.symbol_table , ui_message_handler);
213
- if (instrument_cover_goals (cover_config, goto_model, ui_message_handler))
214
- return true ;
215
- }
216
-
217
- // label the assertions
218
- // This must be done after adding assertions and
219
- // before using the argument of the "property" option.
220
- // Do not re-label after using the property slicer because
221
- // this would cause the property identifiers to change.
222
- label_properties (goto_model);
223
-
224
- // remove any skips introduced since coverage instrumentation
206
+ // remove skips such that trivial GOTOs are deleted and not considered for
207
+ // coverage annotation:
225
208
remove_skip (goto_model);
209
+
210
+ const auto cover_config =
211
+ get_cover_config (options, goto_model.symbol_table , ui_message_handler);
212
+ if (instrument_cover_goals (cover_config, goto_model, ui_message_handler))
213
+ return true ;
226
214
}
227
215
216
+ // label the assertions
217
+ // This must be done after adding assertions and
218
+ // before using the argument of the "property" option.
219
+ // Do not re-label after using the property slicer because
220
+ // this would cause the property identifiers to change.
221
+ label_properties (goto_model);
222
+
223
+ // remove any skips introduced since coverage instrumentation
224
+ remove_skip (goto_model);
225
+
228
226
return false ;
229
227
}
230
228
0 commit comments