@@ -165,66 +165,64 @@ bool jdiff_parse_optionst::process_goto_program(
165165 const optionst &options,
166166 goto_modelt &goto_model)
167167{
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" ))
168205 {
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:
225208 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 ;
226214 }
227215
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+
228226 return false ;
229227}
230228
0 commit comments