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

src/goto-programs/process_goto_program.cpp

@@ -42,11 +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"),
-    false);
+  remove_function_pointers(log.get_message_handler(), goto_model, false);
 
   mm_io(goto_model);
 

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<symbol_exprt, irep_hash> &functions,
-  const bool add_safety_assertion)
+  const std::unordered_set<symbol_exprt, irep_hash> &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;
@@ -542,13 +533,11 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
 void remove_function_pointers(
   message_handlert &_message_handler,
   goto_modelt &goto_model,
-  bool add_safety_assertion,
   bool only_remove_const_fps)
 {
   remove_function_pointerst rfp(
     _message_handler,
     goto_model.symbol_table,
-    add_safety_assertion,
     only_remove_const_fps,
     goto_model.goto_functions);
 

src/goto-programs/remove_function_pointers.h

@@ -28,7 +28,6 @@ class symbol_tablet;
 void remove_function_pointers(
   message_handlert &_message_handler,
   goto_modelt &goto_model,
-  bool add_safety_assertion,
   bool only_remove_const_fps);
 
 /// Replace a call to a dynamic function at location
@@ -40,16 +39,13 @@ void 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<symbol_exprt, irep_hash> &functions,
-  const bool add_safety_assertion);
+  const std::unordered_set<symbol_exprt, irep_hash> &functions);
 
 /// Returns true iff \p call_type can be converted to produce a function call of
 /// the same type as \p function_type.

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