Skip to content

Commit 8e7c656

Browse files
author
martin
committed
Enable the CPROVER library for goto-analyzer
This does change the functionality quite substantially but strangely it only seems to affect one test, and that is syntactic rather than semantic. As with many of the other changes in this PR, I suspect this is swapping one lot of broken, untested functionality for another, slightly less broken but still not working lot of functionality.
1 parent d9ea14b commit 8e7c656

File tree

2 files changed

+9
-14
lines changed

2 files changed

+9
-14
lines changed

regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@ CORE
22
main.c
33
--show-goto-functions --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*IF fp == f1 THEN GOTO [0-9]$
6-
^\s*IF fp == f2 THEN GOTO [0-9]$
7-
^\s*IF fp == f3 THEN GOTO [0-9]$
8-
^\s*IF fp == f4 THEN GOTO [0-9]$
9-
^\s*IF fp == f5 THEN GOTO [0-9]$
10-
^\s*IF fp == f6 THEN GOTO [0-9]$
11-
^\s*IF fp == f7 THEN GOTO [0-9]$
12-
^\s*IF fp == f8 THEN GOTO [0-9]$
13-
^\s*IF fp == f9 THEN GOTO [0-9]$
5+
^\s*IF fp == f1 THEN GOTO [0-9]+$
6+
^\s*IF fp == f2 THEN GOTO [0-9]+$
7+
^\s*IF fp == f3 THEN GOTO [0-9]+$
8+
^\s*IF fp == f4 THEN GOTO [0-9]+$
9+
^\s*IF fp == f5 THEN GOTO [0-9]+$
10+
^\s*IF fp == f6 THEN GOTO [0-9]+$
11+
^\s*IF fp == f7 THEN GOTO [0-9]+$
12+
^\s*IF fp == f8 THEN GOTO [0-9]+$
13+
^\s*IF fp == f9 THEN GOTO [0-9]+$
1414
^EXIT=0$
1515
^SIGNAL=0$
1616
--

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -876,19 +876,14 @@ bool goto_analyzer_parse_optionst::process_goto_program(
876876
// adding the library.
877877
remove_asm(goto_model);
878878

879-
#if 0
880879
// add the library
881880
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
882881
link_to_library(
883882
goto_model, ui_message_handler, cprover_cpp_library_factory);
884883
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
885884

886-
// these are commented out as well because without the library
887-
// this initialization code doesn’t make any sense
888885
add_malloc_may_fail_variable_initializations(goto_model);
889886

890-
#endif
891-
892887
// remove function pointers
893888
log.status() << "Removing function pointers and virtual functions"
894889
<< messaget::eom;

0 commit comments

Comments
 (0)