diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 5e8ce155e8d..ea2c124f93c 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -172,8 +172,7 @@ bool jdiff_parse_optionst::process_goto_program( // remove function pointers log.status() << "Removing function pointers and virtual functions" << messaget::eom; - remove_function_pointers( - ui_message_handler, goto_model, cmdline.isset("pointer-check")); + remove_function_pointers(ui_message_handler, goto_model, false); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc index 64abf7b96fe..1037f47b553 100644 --- a/regression/cbmc-concurrency/pthread_join1/test.desc +++ b/regression/cbmc-concurrency/pthread_join1/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^\[main\.assertion\.1\] line 21 assertion i==1: FAILURE$ ^\[main\.assertion\.2\] line 22 assertion i==2: SUCCESS$ -^\*\* 1 of 2 failed +^\*\* 1 of 3 failed -- ^warning: ignoring diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc index adbd7d687d0..e8fb193f945 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/test.desc +++ b/regression/cbmc-library/pthread_cond_wait-01/test.desc @@ -3,7 +3,7 @@ main.c --bounds-check ^EXIT=10$ ^SIGNAL=0$ -^\*\* 1 of 2 failed +^\*\* 1 of 3 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc index e255c4accf3..3cd78297904 100644 --- a/regression/cbmc/Function_Pointer18/test.desc +++ b/regression/cbmc/Function_Pointer18/test.desc @@ -1,11 +1,12 @@ CORE main.c -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS +\[main.pointer_dereference.1\] line 28 dereferenced function pointer must be f2: FAILURE$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS \[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc index 603d759e8d8..3ed8ac3b6e2 100644 --- a/regression/cbmc/Linking7/member-name-mismatch.desc +++ b/regression/cbmc/Linking7/member-name-mismatch.desc @@ -6,6 +6,6 @@ module2.c ^VERIFICATION FAILED$ line 21 assertion \*g\.a == 42: SUCCESS line 22 assertion \*g\.c == 41: FAILURE -^\*\* 1 of 2 failed +^\*\* 1 of 3 failed -- ^warning: ignoring diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc index 7e8989049b8..2917ed7e4f6 100644 --- a/regression/cbmc/Linking7/test.desc +++ b/regression/cbmc/Linking7/test.desc @@ -4,7 +4,7 @@ module.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 1 of 2 failed +^\*\* 1 of 3 failed line 21 assertion \*g\.a == 42: SUCCESS line 22 assertion \*g\.b == 41: FAILURE -- diff --git a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc index 95cc354a7a2..219d37993c3 100644 --- a/regression/goto-instrument/value-set-fi-fp-removal4/test.desc +++ b/regression/goto-instrument/value-set-fi-fp-removal4/test.desc @@ -1,9 +1,11 @@ CORE test.c --value-set-fi-fp-removal -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ ^file test.c line 20 function main: replacing function pointer by 2 possible targets$ +\[main.pointer_dereference.1\] line 20 dereferenced function pointer must be one of \[(g, f|f, g)\]: FAILURE$ +-- -- This test checks that the value-set-fi-based function pointer removal precisely identifies the function to call for a particular function pointer diff --git a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc index 637e25cc835..954569f642b 100644 --- a/regression/goto-instrument/value-set-fi-fp-removal5/test.desc +++ b/regression/goto-instrument/value-set-fi-fp-removal5/test.desc @@ -1,9 +1,11 @@ CORE test.c --value-set-fi-fp-removal -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ ^file test.c line 19 function main: replacing function pointer by 0 possible targets$ +\[main.pointer_dereference.1\] line 19 no candidates for dereferenced function pointer: FAILURE$ +-- -- This test checks that the value-set-fi-based function pointer removal precisely identifies the function to call for a particular function pointer diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6d635ccedeb..62813340b24 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -945,8 +945,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( function_pointer_removal_done=true; log.status() << "Function Pointer Removal" << messaget::eom; - remove_function_pointers( - ui_message_handler, goto_model, cmdline.isset("pointer-check")); + remove_function_pointers(ui_message_handler, goto_model, false); log.status() << "Virtual function removal" << messaget::eom; remove_virtual_functions(goto_model); log.status() << "Cleaning inline assembler statements" << messaget::eom; @@ -969,7 +968,6 @@ void goto_instrument_parse_optionst::do_remove_const_function_pointers_only() remove_function_pointers( ui_message_handler, goto_model, - cmdline.isset("pointer-check"), true); // abort if we can't resolve via const pointers } diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp index 80e7c10d6f5..0ba50d26470 100644 --- a/src/goto-instrument/value_set_fi_fp_removal.cpp +++ b/src/goto-instrument/value_set_fi_fp_removal.cpp @@ -75,8 +75,7 @@ void value_set_fi_fp_removal( f.second.body, f.first, target, - functions, - true); + functions); } } } diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index bcde95f76f6..baf61980b7f 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -42,10 +42,7 @@ bool process_goto_program( // remove function pointers log.status() << "Removal of function pointers and virtual functions" << messaget::eom; - remove_function_pointers( - log.get_message_handler(), - goto_model, - options.get_bool_option("pointer-check")); + remove_function_pointers(log.get_message_handler(), goto_model, false); mm_io(goto_model); diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 4a4d9d6c129..8ea768eba13 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -37,7 +37,6 @@ class remove_function_pointerst remove_function_pointerst( message_handlert &_message_handler, symbol_tablet &_symbol_table, - bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions); @@ -51,7 +50,6 @@ class remove_function_pointerst message_handlert &message_handler; const namespacet ns; symbol_tablet &symbol_table; - bool add_safety_assertion; // We can optionally halt the FP removal if we aren't able to use // remove_const_function_pointerst to successfully narrow to a small @@ -81,13 +79,11 @@ class remove_function_pointerst remove_function_pointerst::remove_function_pointerst( message_handlert &_message_handler, symbol_tablet &_symbol_table, - bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions) : message_handler(_message_handler), ns(_symbol_table), symbol_table(_symbol_table), - add_safety_assertion(_add_safety_assertion), only_resolve_const_fps(only_resolve_const_fps) { for(const auto &s : symbol_table.symbols) @@ -343,8 +339,7 @@ void remove_function_pointerst::remove_function_pointer( goto_program, function_id, target, - functions, - add_safety_assertion); + functions); } static std::string function_pointer_assertion_comment( @@ -385,8 +380,7 @@ void remove_function_pointer( goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, - const std::unordered_set &functions, - const bool add_safety_assertion) + const std::unordered_set &functions) { const exprt &function = target->call_function(); const exprt &pointer = to_dereference_expr(function).pointer(); @@ -430,14 +424,11 @@ void remove_function_pointer( } // fall-through - if(add_safety_assertion) - { - goto_programt::targett t = - new_code_gotos.add(goto_programt::make_assertion(false_exprt())); - t->source_location_nonconst().set_property_class("pointer dereference"); - t->source_location_nonconst().set_comment( - function_pointer_assertion_comment(functions)); - } + goto_programt::targett t = + new_code_gotos.add(goto_programt::make_assertion(false_exprt())); + t->source_location_nonconst().set_property_class("pointer dereference"); + t->source_location_nonconst().set_comment( + function_pointer_assertion_comment(functions)); new_code_gotos.add(goto_programt::make_assumption(false_exprt())); goto_programt new_code; @@ -539,53 +530,16 @@ void remove_function_pointerst::operator()(goto_functionst &functions) functions.compute_location_numbers(); } -bool remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - goto_programt &goto_program, - const irep_idt &function_id, - bool add_safety_assertion, - bool only_remove_const_fps) -{ - remove_function_pointerst - rfp( - _message_handler, - symbol_table, - add_safety_assertion, - only_remove_const_fps, - goto_functions); - - return rfp.remove_function_pointers(goto_program, function_id); -} - void remove_function_pointers( message_handlert &_message_handler, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, - bool add_safety_assertion, - bool only_remove_const_fps) -{ - remove_function_pointerst - rfp( - _message_handler, - symbol_table, - add_safety_assertion, - only_remove_const_fps, - goto_functions); - - rfp(goto_functions); -} - -void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, - bool add_safety_assertion, bool only_remove_const_fps) { - remove_function_pointers( + remove_function_pointerst rfp( _message_handler, goto_model.symbol_table, - goto_model.goto_functions, - add_safety_assertion, - only_remove_const_fps); + only_remove_const_fps, + goto_model.goto_functions); + + rfp(goto_model.goto_functions); } diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h index ccbfd308847..ea7073a5294 100644 --- a/src/goto-programs/remove_function_pointers.h +++ b/src/goto-programs/remove_function_pointers.h @@ -28,24 +28,7 @@ class symbol_tablet; void remove_function_pointers( message_handlert &_message_handler, goto_modelt &goto_model, - bool add_safety_assertion, - bool only_remove_const_fps=false); - -void remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - goto_functionst &goto_functions, - bool add_safety_assertion, - bool only_remove_const_fps=false); - -bool remove_function_pointers( - message_handlert &_message_handler, - symbol_tablet &symbol_table, - const goto_functionst &goto_functions, - goto_programt &goto_program, - const irep_idt &function_id, - bool add_safety_assertion, - bool only_remove_const_fps = false); + bool only_remove_const_fps); /// Replace a call to a dynamic function at location /// target in the given goto-program by a case-split @@ -56,16 +39,13 @@ bool remove_function_pointers( /// \param function_id: Name of function containing the target /// \param target: location with function call with function pointer /// \param functions: The set of functions to consider -/// \param add_safety_assertion: Iff true, include an assertion that the -// pointer matches one of the candidate functions void remove_function_pointer( message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, - const std::unordered_set &functions, - const bool add_safety_assertion); + const std::unordered_set &functions); /// Returns true iff \p call_type can be converted to produce a function call of /// the same type as \p function_type. diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 56b29c33365..31d9d2905b2 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -79,8 +79,7 @@ static void restrict_function_pointer( goto_program, function_id, location, - candidates, - true); + candidates); } } // namespace