Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 0 additions & 1 deletion regression/acceleration/array_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/array_unsafe2/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/array_unsafe3/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/array_unsafe4/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/const_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/diamond_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/diamond_unsafe2/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/functions_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/multivar_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/nested_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/overflow_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/phases_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/simple_unsafe1/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/simple_unsafe2/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/simple_unsafe3/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/acceleration/simple_unsafe4/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--no-unwinding-assertions

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
1 change: 0 additions & 1 deletion regression/ansi-c/static_inline1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,5 @@ main.c
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$

--
^warning: ignoring
1 change: 0 additions & 1 deletion regression/ansi-c/static_inline2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,5 @@ main.c
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$

--
^warning: ignoring
1 change: 0 additions & 1 deletion regression/cbmc-incr-oneloop/unwind-forever1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,5 @@ main.c
--incremental-check main.0
^EXIT=142$
^SIGNAL=0$

--
^warning: ignoring
1 change: 0 additions & 1 deletion regression/cbmc-incr-oneloop/unwind-forever2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,5 @@ main.c
--incremental-check main.0
^EXIT=142$
^SIGNAL=0$

--
^warning: ignoring
1 change: 0 additions & 1 deletion regression/cbmc-java/tableswitch2/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
table_switch_neg_offset.class
--function table_switch_neg_offset.f

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
1 change: 0 additions & 1 deletion regression/cpp-linter/function-comment-header1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,5 @@ main.cpp

^main\.cpp:26: Could not find function header comment for foo \[readability/function_comment\] \[4\]
^Total errors found: 1$

^SIGNAL=0$
--
1 change: 0 additions & 1 deletion regression/cpp-linter/struct-inline-decl/test.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.cpp


^Total errors found: 0$
^EXIT=0$
^SIGNAL=0$
Expand Down
19 changes: 9 additions & 10 deletions regression/goto-analyzer/approx-array-variable-const-fp/test.desc
Original file line number Diff line number Diff line change
@@ -1,17 +1,16 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp_tbl\[\(signed long int\)i\] == f2 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f3 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f4 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
^SIGNAL=0$
--
^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f5 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f6 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f7 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
^warning: ignoring
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\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,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\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,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\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,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\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,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\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,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == \(const void_fp\)f2 THEN GOTO [0-9]$
^\s*IF fp == \(const void_fp\)f3 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp2 == f1 THEN GOTO [0-9]$
^\s*IF fp2 == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF \*fp == f1 THEN GOTO [0-9]$
^\s*IF \*fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
^SIGNAL=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*ASSERT FALSE // invalid function pointer$
^SIGNAL=0$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF final_fp == f1 THEN GOTO [0-9]$
^\s*IF final_fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
CORE
main.c
--show-goto-functions --verbosity 10 --pointer-check

^Removing function pointers and virtual functions$
^\s*IF fp == f1 THEN GOTO [0-9]$
^\s*IF fp == f2 THEN GOTO [0-9]$
Expand Down
Loading