diff --git a/regression/cprover/function_calls/function_pointer1.desc b/regression/cprover/function_calls/function_pointer1.desc index 2ec13934978..cd13c1a5ebc 100644 --- a/regression/cprover/function_calls/function_pointer1.desc +++ b/regression/cprover/function_calls/function_pointer1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE function_pointer1.c --safety ^EXIT=10$ diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index b4ca605f357..0acf3255824 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/src/cprover/cprover_parse_options.cpp @@ -144,10 +144,8 @@ int cprover_parse_optionst::main() ? static_cast(message_handler) : static_cast(null_message_handler); - const bool safety = !cmdline.isset("no-safety"); - remove_function_pointers( - remove_function_pointers_message_handler, goto_model, safety); + remove_function_pointers_message_handler, goto_model, false); adjust_float_expressions(goto_model); instrument_given_invariants(goto_model); @@ -166,7 +164,7 @@ int cprover_parse_optionst::main() if(!perform_inlining) instrument_contracts(goto_model); - if(safety) + if(!cmdline.isset("no-safety")) c_safety_checks(goto_model); if(cmdline.isset("no-assertions"))