Skip to content

Commit 3b00bdc

Browse files
committed
Fix tests with missing EXIT or SIGNAL tests
Some tests had previously been passing despite actually causing a crash, due to the required output being too loosely specified. This ensures the bare minimum: that every test has an expected EXIT code and SIGNAL result. The codes suggested were taken from the test's current output, and only applied for CORE tests, but hand inspection suggests these choices are reasonable.
1 parent 7b56203 commit 3b00bdc

File tree

167 files changed

+264
-3
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

167 files changed

+264
-3
lines changed

regression/ansi-c/Forward_Declaration2/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
CORE
22
main.c
33

4+
^EXIT=(1|64)$
45
^SIGNAL=0$
56
^CONVERSION ERROR$
67
--

regression/ansi-c/Incomplete_Type1/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
CORE
22
main.c
33

4+
^EXIT=(1|64)$
45
^SIGNAL=0$
56
^CONVERSION ERROR$
67
--

regression/ansi-c/function_return1/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ CORE
22
main.c
33
--verbosity 2
44
^main.c:3:1: warning: function has return void but a return statement returning signed int$
5+
^EXIT=0$
56
^SIGNAL=0$
67
--
78
^warning: ignoring

regression/ansi-c/static2/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ CORE
22
main.c
33
main2.c --function foo
44
^main symbol `foo' is ambiguous$
5+
^EXIT=(1|64)$
6+
^SIGNAL=0$
57
--
68
^warning: ignoring

regression/ansi-c/static3/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ CORE
22
main.c
33
main2.c --function foo
44
^main symbol `foo' is ambiguous$
5+
^EXIT=(1|64)$
6+
^SIGNAL=0$
57
--
68
^warning: ignoring

regression/cbmc-java/NondetArray/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ CORE
22
NondetArray.class
33
--function NondetArray.main
44
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
^warning: ignoring

regression/cbmc-java/NondetArray2/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetArray2.class
33
--function NondetArray2.main --unwind 5
44
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
--
79
Disabled pending fixing warnings for array-of with zero length:

regression/cbmc-java/NondetArray3/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE
22
NondetArray3.class
33
--function NondetArray3.main --unwind 5
44
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
--
79
Disabled pending fixing warnings for array-of with zero length:

regression/cbmc-java/NondetArray4/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ CORE
22
NondetArray4.class
33
--function NondetArray4.main
44
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
^warning: ignoring

regression/cbmc-java/NondetAssume1/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ CORE
22
NondetAssume1.class
33
--function NondetAssume1.main
44
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
57
--
68
^warning: ignoring

0 commit comments

Comments
 (0)