Skip to content

Refactor process_goto_program so that all tools use common processing code #5807

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 21 commits into from
Feb 23, 2021
Merged
Show file tree
Hide file tree
Changes from 20 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
8ca930d
Create a stub for a common process_goto_program
Feb 1, 2021
ac1298e
Add remove_asm to goto-analyzer to make program processing more consi…
Feb 2, 2021
6fdf17e
Enable the CPROVER library for goto-analyzer
Feb 3, 2021
ca4d720
Add 'malloc may fail' initialization to goto-diff
Feb 3, 2021
5ce65ad
Add string abstraction to goto-analyzer and goto-diff
Feb 3, 2021
41def5e
Replace the use of cmdline with options in goto-analyzer and goto-diff
Feb 3, 2021
8d68a63
Replace the parsing of goto_check options with the appropriate macro
Feb 3, 2021
797cd1e
Add memory mapped IO support to goto-analyzer
Feb 13, 2021
ea2792d
Add partial inlining as an optional part of process_goto_program
Feb 6, 2021
bc11a05
Make the call to rewrite-union configurable
Feb 6, 2021
415c1a3
Add options that goto-check uses to the macros
Feb 6, 2021
f48a4dc
Enable goto_check in goto-analyzer
Feb 6, 2021
75509bf
goto-analyzer now adds the rounding mode to floating-point operations
Feb 7, 2021
69927c4
More string abstraction to be common processing of goto-programs
Feb 8, 2021
527917c
Move the update functions earlier so that they are common between tools
Feb 8, 2021
00aacd8
Change the text of the logging message so that it is the same as CBMC
Feb 13, 2021
bb3dcb4
Move the majority of process_goto_program out of the individual tools
Feb 13, 2021
7fb0e7a
Fix up the doxygen warnings
Feb 13, 2021
e09efcb
Fix unit test that uses some, but not all, of CBMC's option parsing
Feb 22, 2021
a6c720b
Enabling goto_check in goto-analyzer adds 7 instructions to the test
Feb 22, 2021
c4db021
Fix typo in comments
martin-cs Feb 22, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$
^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$
^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
^EXIT=0$
^SIGNAL=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
^\s*IF \*fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
^\s*IF fp2 == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
^\s*IF fp2 == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
^\s*IF \*fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
^\s*IF \*fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
^EXIT=0$
^SIGNAL=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
replacing function pointer by 9 possible targets
^EXIT=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
replacing function pointer by 9 possible targets
^EXIT=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF final_fp == f1 THEN GOTO [0-9]$
^\s*IF final_fp == f2 THEN GOTO [0-9]$
^\s*IF final_fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
^\s*IF fp == f4 THEN GOTO [0-9]$
^\s*IF fp == f5 THEN GOTO [0-9]$
^\s*IF fp == f6 THEN GOTO [0-9]$
^\s*IF fp == f7 THEN GOTO [0-9]$
^\s*IF fp == f8 THEN GOTO [0-9]$
^\s*IF fp == f9 THEN GOTO [0-9]$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]+$
^\s*IF fp == f2 THEN GOTO [0-9]+$
^\s*IF fp == f3 THEN GOTO [0-9]+$
^\s*IF fp == f4 THEN GOTO [0-9]+$
^\s*IF fp == f5 THEN GOTO [0-9]+$
^\s*IF fp == f6 THEN GOTO [0-9]+$
^\s*IF fp == f7 THEN GOTO [0-9]+$
^\s*IF fp == f8 THEN GOTO [0-9]+$
^\s*IF fp == f9 THEN GOTO [0-9]+$
^EXIT=0$
^SIGNAL=0$
--
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
^\s*IF fp2 == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-analyzer/no-match-const-fp-null/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
function func: replacing function pointer by 0 possible targets
^EXIT=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF container_pointer->fp == f1 THEN GOTO [0-9]$
^\s*IF container_pointer->fp == f2 THEN GOTO [0-9]$
^\s*IF container_pointer->fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF pts->go == f1 THEN GOTO [0-9]$
^\s*IF pts->go == f2 THEN GOTO [0-9]$
^\s*IF pts->go == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
^EXIT=0$
^SIGNAL=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$
^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$
^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$
^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$
^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
^\s*IF fp2 == f3 THEN GOTO [0-9]$
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-analyzer/no-match-non-const-fp/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-analyzer/no-match-parameter-fp/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
^\s*IF fp == f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
main.c
--show-goto-functions --pointer-check
^Removing function pointers and virtual functions$
^Removal of function pointers and virtual functions$
^\s*IF container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$
^\s*IF container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$
^\s*IF container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$
Expand Down
Loading