diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc index cf57f120e27..82860e90e86 100644 --- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc index d2d1e6e7c5b..5b970303b37 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc index 794cc54b854..bd1f5b41a5d 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc index d2d1e6e7c5b..5b970303b37 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index d2d1e6e7c5b..5b970303b37 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc index d2d1e6e7c5b..5b970303b37 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc index 2ccd4a4d80a..57386e3d576 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc index 22363df6f7d..b687a13cf86 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index 81cd4f80322..25c0e72dadf 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc index 45ca8ea9da3..a439885fc9c 100644 --- a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc index 8e2ce9fde50..1fb62392ced 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc index 8e2ce9fde50..1fb62392ced 100644 --- a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc index 45ca8ea9da3..a439885fc9c 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc index 45ca8ea9da3..a439885fc9c 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index e3e3a8e85d2..da6211eba82 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index e0da8d71617..24ca16f13c1 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index e0da8d71617..24ca16f13c1 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc index 9b89705e266..4b204902e0b 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc index 778aa7a3af6..c1c2246e027 100644 --- a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc @@ -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$ -- diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc index 8e2ce9fde50..1fb62392ced 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index edafa34c83d..0abb9994d73 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc index 6b453835cc7..39b4bf06fa6 100644 --- a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc index 049c5ef7617..c2854d7bb90 100644 --- a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index e3e3a8e85d2..da6211eba82 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc @@ -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$ diff --git a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc index 43a80cd16d6..63c375d058a 100644 --- a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc index a3e6aac6078..7c7f7c5d265 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc index a3e6aac6078..7c7f7c5d265 100644 --- a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc index 8e2ce9fde50..1fb62392ced 100644 --- a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-non-const-fp/test.desc b/regression/goto-analyzer/no-match-non-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-parameter-fp/test.desc b/regression/goto-analyzer/no-match-parameter-fp/test.desc index 778aa7a3af6..9fc199c2365 100644 --- a/regression/goto-analyzer/no-match-parameter-fp/test.desc +++ b/regression/goto-analyzer/no-match-parameter-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc index a7341164b17..ca24699d5a0 100644 --- a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc +++ b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc @@ -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]$ diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc index a50db503948..791dbe0703c 100644 --- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc index b0a7231d519..479c26e4afe 100644 --- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc @@ -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*f2\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc index a50db503948..791dbe0703c 100644 --- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc index c138bc77f3d..15fc1e17ef7 100644 --- a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc +++ b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc index a50db503948..791dbe0703c 100644 --- a/regression/goto-analyzer/precise-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-fp/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc index b0a7231d519..479c26e4afe 100644 --- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc +++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc @@ -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*f2\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc index a50db503948..791dbe0703c 100644 --- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc +++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc index a50db503948..791dbe0703c 100644 --- a/regression/goto-analyzer/precise-derefence/test.desc +++ b/regression/goto-analyzer/precise-derefence/test.desc @@ -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*f2\(\); ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc index 19aa299e481..02bf70c4391 100644 --- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc +++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc @@ -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*f3\(\);$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index d56acd449f3..c7418935086 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc @@ -5,7 +5,7 @@ main.c ^file main.c line 46 function main: replacing function pointer by 2 possible targets$ ^file main.c line 54 function main: replacing function pointer by 2 possible targets$ ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end -^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[23, 25\]} @ \[23, 25\] +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[30, 32\]} @ \[30, 32\] ^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 314cc2cf55f..2b3353658a7 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -79,10 +79,9 @@ /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp:188: warning: The following parameter of initialize_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration) is not documented: parameter 'configuration' -warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. @@ -91,7 +90,7 @@ warning: Included by graph for 'expr.h' not generated, too many nodes (87), thre warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (101), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index fe5b0099983..aafc6f5b435 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -40,7 +40,10 @@ void goto_check( "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ "(pointer-primitive-check)" \ - "(retain-trivial-checks)" + "(retain-trivial-checks)" \ + "(error-label):" \ + "(no-assertions)(no-assumptions)" \ + "(assert-to-assume)" // clang-format off #define HELP_GOTO_CHECK \ @@ -59,6 +62,11 @@ void goto_check( " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \ " --no-built-in-assertions ignore assertions in built-in library\n" \ " --retain-trivial-checks include checks that are trivially true\n" \ + " --error-label label check that label is unreachable\n" \ + " --no-built-in-assertions ignore assertions in built-in library\n" \ + " --no-assertions ignore user assertions\n" \ + " --no-assumptions ignore user assumptions\n" \ + " --assert-to-assume convert user assertions to assumptions\n" \ #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ @@ -77,6 +85,12 @@ void goto_check( options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial-checks", \ cmdline.isset("retain-trivial-checks")); \ + options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \ + if(cmdline.isset("error-label")) \ + options.set_option("error-label", cmdline.get_values("error-label")); \ (void)0 // clang-format on diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d9f6a884ba2..b81f38b7ecb 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -49,26 +49,18 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include -#include #include #include -#include +#include #include -#include -#include -#include #include #include -#include -#include #include #include #include #include -#include -#include #include #include @@ -112,8 +104,6 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( void cbmc_parse_optionst::set_default_options(optionst &options) { // Default true - options.set_option("assertions", true); - options.set_option("assumptions", true); options.set_option("built-in-assertions", true); options.set_option("pretty-names", true); options.set_option("propagation", true); @@ -311,18 +301,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); - // generate unwinding assertions if(cmdline.isset("unwinding-assertions")) { @@ -529,6 +507,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-points-to-sets", true); PARSE_OPTIONS_GOTO_TRACE(cmdline, options); + + // Options for process_goto_program + options.set_option("rewrite-union", true); } /// invoke main modules @@ -926,34 +907,9 @@ bool cbmc_parse_optionst::process_goto_program( add_malloc_may_fail_variable_initializations(goto_model); - if(options.get_bool_option("string-abstraction")) - string_instrumentation(goto_model); - - // remove function pointers - log.status() << "Removal of function pointers and virtual functions" - << messaget::eom; - remove_function_pointers( - log.get_message_handler(), - goto_model, - options.get_bool_option("pointer-check")); - - mm_io(goto_model); - - // instrument library preconditions - instrument_preconditions(goto_model); - - // remove returns, gcc vectors, complex - remove_returns(goto_model); - remove_vector(goto_model); - remove_complex(goto_model); - rewrite_union(goto_model); - - // add generic checks - log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); - - // checks don't know about adjusted float expressions - adjust_float_expressions(goto_model); + // Common removal of types and complex constructs + if(::process_goto_program(goto_model, options, log)) + return true; // ignore default/user-specified initialization // of variables with static lifetime @@ -965,22 +921,10 @@ bool cbmc_parse_optionst::process_goto_program( nondet_static(goto_model); } - if(options.get_bool_option("string-abstraction")) - { - log.status() << "String Abstraction" << messaget::eom; - string_abstraction(goto_model, log.get_message_handler()); - } - // add failed symbols // needs to be done before pointer analysis add_failed_symbols(goto_model.symbol_table); - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - if(options.get_bool_option("drop-unused-functions")) { // Entry point will have been set before and function pointers removed @@ -1119,9 +1063,6 @@ void cbmc_parse_optionst::help() "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --error-label label check that label is unreachable\n" HELP_COVER " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) // NOLINTNEXTLINE(whitespace/line_length) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index af9e265f782..61b960c152d 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -53,7 +53,6 @@ class optionst; "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ "(object-bits):" \ OPT_GOTO_CHECK \ - "(no-assertions)(no-assumptions)" \ "(malloc-fail-assert)(malloc-fail-null)" \ "(malloc-may-fail)" \ OPT_XML_INTERFACE \ @@ -73,7 +72,7 @@ class optionst; "(drop-unused-functions)" \ "(havoc-undefined-functions)" \ "(property):(stop-on-fail)(trace)" \ - "(error-label):(verbosity):(no-library)" \ + "(verbosity):(no-library)" \ "(nondet-static)" \ "(version)" \ OPT_COVER \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 1b5b72848a4..468a1b94124 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -27,16 +27,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include #include +#include #include -#include -#include -#include -#include #include #include #include @@ -125,23 +121,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) config.cpp.set_cpp11(); #endif -#if 0 - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); -#endif + // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // The user should either select: // 1. a specific analysis, or @@ -600,6 +581,10 @@ int goto_analyzer_parse_optionst::doit() goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options); + // Preserve backwards compatibility in processing + options.set_option("partial-inline", true); + options.set_option("rewrite-union", false); + if(process_goto_program(options)) return CPROVER_EXIT_INTERNAL_ERROR; @@ -631,7 +616,6 @@ int goto_analyzer_parse_optionst::doit() /// Depending on the command line mode, run one of the analysis tasks int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) { - adjust_float_expressions(goto_model); if(options.get_bool_option("taint")) { std::string taint_file=cmdline.get_value("taint"); @@ -867,53 +851,22 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) bool goto_analyzer_parse_optionst::process_goto_program( const optionst &options) { - { - #if 0 - // Remove inline assembler; this needs to happen before - // adding the library. - remove_asm(goto_model); + // Remove inline assembler; this needs to happen before + // adding the library. + remove_asm(goto_model); - // add the library - log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom; - link_to_library( - goto_model, ui_message_handler, cprover_cpp_library_factory); - link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); - - // these are commented out as well because without the library - // this initialization code doesn’t make any sense - add_malloc_may_fail_variable_initializations(goto_model); - -#endif + // add the library + log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" + << messaget::eom; + link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory); + link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); - // remove function pointers - log.status() << "Removing function pointers and virtual functions" - << messaget::eom; - remove_function_pointers( - ui_message_handler, goto_model, cmdline.isset("pointer-check")); + add_malloc_may_fail_variable_initializations(goto_model); - // do partial inlining - log.status() << "Partial Inlining" << messaget::eom; - goto_partial_inline(goto_model, ui_message_handler); + // Common removal of types and complex constructs + if(::process_goto_program(goto_model, options, log)) + return true; - // remove returns, gcc vectors, complex - remove_returns(goto_model); - remove_vector(goto_model); - remove_complex(goto_model); - -#if 0 - // add generic checks - log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); -#else - (void)options; // unused parameter -#endif - - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - } return false; } diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index f0478bd24c4..5df534f126f 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -24,6 +24,7 @@ Author: Peter Schrammel #include +#include #include #include #include @@ -32,6 +33,7 @@ Author: Peter Schrammel #include #include #include +#include #include #include #include @@ -128,69 +130,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) else options.set_option("propagation", true); - // check array bounds - if(cmdline.isset("bounds-check")) - options.set_option("bounds-check", true); - else - options.set_option("bounds-check", false); - - // check division by zero - if(cmdline.isset("div-by-zero-check")) - options.set_option("div-by-zero-check", true); - else - options.set_option("div-by-zero-check", false); - - // check overflow/underflow - if(cmdline.isset("signed-overflow-check")) - options.set_option("signed-overflow-check", true); - else - options.set_option("signed-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("unsigned-overflow-check")) - options.set_option("unsigned-overflow-check", true); - else - options.set_option("unsigned-overflow-check", false); - - // check overflow/underflow - if(cmdline.isset("float-overflow-check")) - options.set_option("float-overflow-check", true); - else - options.set_option("float-overflow-check", false); - - // check for NaN (not a number) - if(cmdline.isset("nan-check")) - options.set_option("nan-check", true); - else - options.set_option("nan-check", false); - - // check pointers - if(cmdline.isset("pointer-check")) - options.set_option("pointer-check", true); - else - options.set_option("pointer-check", false); - - // check for memory leaks - if(cmdline.isset("memory-leak-check")) - options.set_option("memory-leak-check", true); - else - options.set_option("memory-leak-check", false); - - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); + // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // generate unwinding assertions if(cmdline.isset("cover")) @@ -212,6 +153,9 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) } options.set_option("show-properties", cmdline.isset("show-properties")); + + // Options for process_goto_program + options.set_option("rewrite-union", true); } /// invoke main modules @@ -314,72 +258,45 @@ bool goto_diff_parse_optionst::process_goto_program( const optionst &options, goto_modelt &goto_model) { + // Remove inline assembler; this needs to happen before + // adding the library. + remove_asm(goto_model); + + // add the library + log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" + << messaget::eom; + link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory); + link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); + + add_malloc_may_fail_variable_initializations(goto_model); + + // Common removal of types and complex constructs + if(::process_goto_program(goto_model, options, log)) + return true; + + // instrument cover goals + if(cmdline.isset("cover")) { - // Remove inline assembler; this needs to happen before - // adding the library. - remove_asm(goto_model); - - // add the library - log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" - << messaget::eom; - link_to_library( - goto_model, ui_message_handler, cprover_cpp_library_factory); - link_to_library(goto_model, ui_message_handler, cprover_c_library_factory); - - // remove function pointers - log.status() << "Removal of function pointers and virtual functions" - << messaget::eom; - remove_function_pointers( - ui_message_handler, goto_model, cmdline.isset("pointer-check")); - - mm_io(goto_model); - - // instrument library preconditions - instrument_preconditions(goto_model); - - // remove returns, gcc vectors, complex - remove_returns(goto_model); - remove_vector(goto_model); - remove_complex(goto_model); - rewrite_union(goto_model); - - // add generic checks - log.status() << "Generic Property Instrumentation" << messaget::eom; - goto_check(options, goto_model); - - // checks don't know about adjusted float expressions - adjust_float_expressions(goto_model); - - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - - // instrument cover goals - if(cmdline.isset("cover")) - { - // remove skips such that trivial GOTOs are deleted and not considered - // for coverage annotation: - remove_skip(goto_model); - - const auto cover_config = - get_cover_config(options, goto_model.symbol_table, ui_message_handler); - if(instrument_cover_goals(cover_config, goto_model, ui_message_handler)) - return true; - } - - // label the assertions - // This must be done after adding assertions and - // before using the argument of the "property" option. - // Do not re-label after using the property slicer because - // this would cause the property identifiers to change. - label_properties(goto_model); - - // remove any skips introduced since coverage instrumentation + // remove skips such that trivial GOTOs are deleted and not considered + // for coverage annotation: remove_skip(goto_model); + + const auto cover_config = + get_cover_config(options, goto_model.symbol_table, ui_message_handler); + if(instrument_cover_goals(cover_config, goto_model, ui_message_handler)) + return true; } + // label the assertions + // This must be done after adding assertions and + // before using the argument of the "property" option. + // Do not re-label after using the property slicer because + // this would cause the property identifiers to change. + label_properties(goto_model); + + // remove any skips introduced since coverage instrumentation + remove_skip(goto_model); + return false; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2e1f16a10dd..00119a4877f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1010,31 +1010,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() else options.set_option("simplify", true); - // use assumptions instead of assertions? - if(cmdline.isset("assert-to-assume")) - options.set_option("assert-to-assume", true); - else - options.set_option("assert-to-assume", false); - // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_value("error-label")); - // unwind loops if(cmdline.isset("unwind")) { @@ -1806,7 +1784,6 @@ void goto_instrument_parse_optionst::help() " --no-assertions ignore user assertions\n" HELP_GOTO_CHECK " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*) - " --error-label label check that label is unreachable\n" " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*) " --race-check add floating-point data race checks\n" "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 353b8a1e8f1..4dae4e0ca70 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -52,8 +52,7 @@ Author: Daniel Kroening, kroening@kroening.com "(no-nan-check)" \ "(remove-pointers)" \ "(no-simplify)" \ - "(assert-to-assume)" \ - "(no-assertions)(no-assumptions)(uninitialized-check)" \ + "(uninitialized-check)" \ "(race-check)(scc)(one-event-per-cycle)" \ "(minimum-interference)" \ "(mm):(my-events)" \ @@ -92,7 +91,7 @@ Author: Daniel Kroening, kroening@kroening.com "(cav11)" \ OPT_TIMESTAMP \ "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \ - "(error-label):(string-abstraction)" \ + "(string-abstraction)" \ "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \ "(accelerate)(constant-propagator)" \ "(k-induction):(step-case)(base-case)" \ diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 18a9129e7be..1ad85c9b469 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -39,6 +39,7 @@ SRC = add_malloc_may_fail_variable_initializations.cpp \ parameter_assignments.cpp \ pointer_arithmetic.cpp \ printf_formatter.cpp \ + process_goto_program.cpp \ read_bin_goto_object.cpp \ read_goto_binary.cpp \ rebuild_goto_start_function.cpp \ diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp new file mode 100644 index 00000000000..68121ab9335 --- /dev/null +++ b/src/goto-programs/process_goto_program.cpp @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: Process a Goto Program + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +/// \file +/// Get a Goto Program + +#include "process_goto_program.h" + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +bool process_goto_program( + goto_modelt &goto_model, + const optionst &options, + messaget &log) +{ + if(options.get_bool_option("string-abstraction")) + string_instrumentation(goto_model); + + // remove function pointers + log.status() << "Removal of function pointers and virtual functions" + << messaget::eom; + remove_function_pointers( + log.get_message_handler(), + goto_model, + options.get_bool_option("pointer-check")); + + mm_io(goto_model); + + // instrument library preconditions + instrument_preconditions(goto_model); + + // do partial inlining + if(options.get_bool_option("partial-inline")) + { + log.status() << "Partial Inlining" << messaget::eom; + goto_partial_inline(goto_model, log.get_message_handler()); + } + + // remove returns, gcc vectors, complex + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + if(options.get_bool_option("rewrite-union")) + rewrite_union(goto_model); + + // add generic checks + log.status() << "Generic Property Instrumentation" << messaget::eom; + goto_check(options, goto_model); + + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); + + if(options.get_bool_option("string-abstraction")) + { + log.status() << "String Abstraction" << messaget::eom; + string_abstraction(goto_model, log.get_message_handler()); + } + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + // add loop ids + goto_model.goto_functions.compute_loop_numbers(); + + return false; +} diff --git a/src/goto-programs/process_goto_program.h b/src/goto-programs/process_goto_program.h new file mode 100644 index 00000000000..a3f18b27a34 --- /dev/null +++ b/src/goto-programs/process_goto_program.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Process a Goto Program + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H +#define CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H + +class goto_modelt; +class optionst; +class messaget; + +/// Common processing and simplification of goto_programts. +/// This includes removing a number of more complex types +/// (vectors, complex, etc.) and constructs +/// (returns, function pointers, etc.). +/// This is can be used after initialize_goto_model but before +/// analysis. It is not mandatory but is used by most tools. +bool process_goto_program( + goto_modelt &goto_model, + const optionst &options, + messaget &log); + +#endif // CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index a3cb3a23ad9..ed8887a67fc 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -384,6 +384,8 @@ void _check_with_strategy( optionst options; cbmc_parse_optionst::set_default_options(options); + options.set_option("assertions", true); + options.set_option("assumptions", true); options.set_option("paths", true); options.set_option("exploration-strategy", strategy); REQUIRE(is_valid_path_strategy(strategy));