Enable the function-pointer fall-back assertion by default

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

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

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

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