Enable the function-pointer fall-back assertion by default

Function pointer removal may be done implicitly as required by some
other operation that the user intended to do. If so, the user would not
know that they need to specify --pointer-check at that point. Therefore,
enable the `ASSERT(false)` in the `else` branch of function pointer
removal unconditionally.

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"), false);
+  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"), false);
+  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);
           }
         }
       }