Merge pull request #7011 from tautschnig/bugfixes/6983-take-2

Enable the function-pointer fall-back assertion by default

Author: tautschnig

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);

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

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

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

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

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
 --

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

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

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
 }
 

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);
           }
         }
       }