Skip to content

Commit c3983b5

Browse files
author
martin
committed
Enable goto_check in goto-analyzer
This was included in the options that goto-analyzer recognises and in its --help output but they were all silently ignored. This commit fixes that so that they are supported, making it more consistent with CBMC (and less inexplicable).
1 parent 71a42d7 commit c3983b5

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -906,13 +906,9 @@ bool goto_analyzer_parse_optionst::process_goto_program(
906906
if(options.get_bool_option("rewrite-union"))
907907
rewrite_union(goto_model);
908908

909-
#if 0
910909
// add generic checks
911910
log.status() << "Generic Property Instrumentation" << messaget::eom;
912911
goto_check(options, goto_model);
913-
#else
914-
(void)options; // unused parameter
915-
#endif
916912

917913
// recalculate numbers, etc.
918914
goto_model.goto_functions.update();

0 commit comments

Comments
 (0)