Remove undefined-function-is-assume-false from goto-instrument

Users can like-for-like replace such use with
`--generate-function-body '.*' --generate-function-body-options assume-false`.

Fixes: #2070

Author: tautschnig

doc/man/goto-instrument.1

@@ -414,9 +414,6 @@ prepends a call to \fIcallee\fR in the body of \fIcaller\fR
 instruments checks to assert that all call
 sequences match \fIseq\fR
 .TP
-\fB\-\-undefined\-function\-is\-assume\-false\fR
-convert each call to an undefined function to assume(false)
-.TP
 \fB\-\-insert\-final\-assert\-false\fR \fIfunction\fR
 generate assert(false) at end of \fIfunction\fR
 .TP

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -911,12 +911,6 @@ int goto_instrument_parse_optionst::doit()
       remove_unused_functions(goto_model.goto_functions, ui_message_handler);
     }
 
-    if(cmdline.isset("undefined-function-is-assume-false"))
-    {
-      do_indirect_call_and_rtti_removal();
-      undefined_function_abort_path(goto_model);
-    }
-
     // write new binary?
     if(cmdline.args.size()==2)
     {
@@ -1959,8 +1953,6 @@ void goto_instrument_parse_optionst::help()
     " the body of {ucaller}\n"
     " {y--check-call-sequence} {useq} \t instruments checks to assert that all"
     " call sequences match {useq}\n"
-    " {y--undefined-function-is-assume-false} \t convert each call to an"
-    " undefined function to assume(false)\n"
     HELP_INSERT_FINAL_ASSERT_FALSE
     HELP_REPLACE_FUNCTION_BODY
     HELP_RESTRICT_FUNCTION_POINTER

src/goto-instrument/goto_instrument_parse_options.h

@@ -109,7 +109,6 @@ Author: Daniel Kroening, [email protected]
   "(" FLAG_ENFORCE_CONTRACT "):" \
   OPT_ENFORCE_CONTRACT_REC \
   "(show-threaded)(list-calls-args)" \
-  "(undefined-function-is-assume-false)" \
   "(remove-function-body):" \
   "(remove-function-body-regex):" \
   OPT_AGGRESSIVE_SLICER \

src/goto-instrument/undefined_functions.cpp

@@ -31,37 +31,3 @@ void list_undefined_functions(
       os << gf_entry.first << '\n';
   }
 }
-
-void undefined_function_abort_path(goto_modelt &goto_model)
-{
-  for(auto &gf_entry : goto_model.goto_functions.function_map)
-  {
-    for(auto &ins : gf_entry.second.body.instructions)
-    {
-      if(!ins.is_function_call())
-        continue;
-
-      const auto &function = ins.call_function();
-
-      if(function.id() != ID_symbol)
-        continue;
-
-      const irep_idt &function_identifier =
-        to_symbol_expr(function).get_identifier();
-
-      goto_functionst::function_mapt::const_iterator entry =
-        goto_model.goto_functions.function_map.find(function_identifier);
-      DATA_INVARIANT(
-        entry!=goto_model.goto_functions.function_map.end(),
-        "called function must be in function_map");
-
-      if(entry->second.body_available())
-        continue;
-
-      source_locationt annotated_location = ins.source_location();
-      annotated_location.set_comment(
-        "'" + id2string(function_identifier) + "' is undefined");
-      ins = goto_programt::make_assumption(false_exprt(), annotated_location);
-    }
-  }
-}

src/goto-instrument/undefined_functions.h

@@ -22,6 +22,4 @@ void list_undefined_functions(
   const goto_modelt &,
   std::ostream &);
 
-void undefined_function_abort_path(goto_modelt &);
-
 #endif