Skip to content

Commit 1383819

Browse files
authored
Merge pull request #7183 from diffblue/fix-function-pointer-removal
CHC encoder: fix function pointer removal
2 parents a996331 + 2a08d59 commit 1383819

File tree

2 files changed

+3
-5
lines changed

2 files changed

+3
-5
lines changed

regression/cprover/function_calls/function_pointer1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
function_pointer1.c
33
--safety
44
^EXIT=10$

src/cprover/cprover_parse_options.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -144,10 +144,8 @@ int cprover_parse_optionst::main()
144144
? static_cast<message_handlert &>(message_handler)
145145
: static_cast<message_handlert &>(null_message_handler);
146146

147-
const bool safety = !cmdline.isset("no-safety");
148-
149147
remove_function_pointers(
150-
remove_function_pointers_message_handler, goto_model, safety);
148+
remove_function_pointers_message_handler, goto_model, false);
151149

152150
adjust_float_expressions(goto_model);
153151
instrument_given_invariants(goto_model);
@@ -166,7 +164,7 @@ int cprover_parse_optionst::main()
166164
if(!perform_inlining)
167165
instrument_contracts(goto_model);
168166

169-
if(safety)
167+
if(!cmdline.isset("no-safety"))
170168
c_safety_checks(goto_model);
171169

172170
if(cmdline.isset("no-assertions"))

0 commit comments

Comments
 (0)