Skip to content

Commit 73c3384

Browse files
committed
results now include line number
1 parent 3028bf8 commit 73c3384

File tree

44 files changed

+153
-145
lines changed

Some content is hidden

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

44 files changed

+153
-145
lines changed

jbmc/regression/jbmc/catch1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ catch1.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
^\[.*\] no uncaught exception: FAILURE$
7+
^\[.*\] line 15 no uncaught exception: FAILURE$
88
--
99
^warning: ignoring
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
Primary.class
33
--function Primary.main
4-
^\[java::Primary.Run:\(\)V\.assertion\.1\] assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
4+
^\[java::Primary.Run:\(\)V\.assertion\.1\] line 6 assertion at file Primary\.java line 6 function java::Primary.Run:\(\)V bytecode-index 22: FAILURE$
55
^VERIFICATION FAILED$
66
--
77
^warning: ignoring

regression/cbmc/Array_operations1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[test_copy\.assertion\.4\] expected to fail: FAILURE$
6+
^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
77
^\*\* 1 of 8 failed
88
^VERIFICATION FAILED$
99
--

regression/cbmc/Function5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--pointer-check --bounds-check
44
^SIGNAL=0$
55
^EXIT=10$
6-
^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$
6+
^\[.*\] .* dereference failure: pointer outside object bounds in \*p: FAILURE$
77
--
88
^warning: ignoring

regression/cbmc/Multi_Dimensional_Array6/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--unwind 3 --no-unwinding-assertions
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.assertion\.1\] : SUCCESS$
7-
^\[main\.assertion\.2\] : FAILURE$
6+
^\[main\.assertion\.1\] .* : SUCCESS$
7+
^\[main\.assertion\.2\] .* : FAILURE$
88
^\*\* 1 of 2 failed
99
--
1010
^warning: ignoring

regression/cbmc/Multiple_Properties1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$
8-
^main.c function main\n\[main\.assertion\.1\] .* SUCCESS\n\[main\.assertion\.3\] .* FAILURE$
8+
^main.c function main\n\[main\.assertion\.1\] line 5 .* SUCCESS\n\[main\.assertion\.3\] line 9 .* FAILURE$
99
--
1010
^warning: ignoring

regression/cbmc/Overflow_Addition1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--signed-overflow-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[.*\] arithmetic overflow on signed \+ in .*: FAILURE$
6+
^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

regression/cbmc/Overflow_Leftshift1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--signed-overflow-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[.*\] arithmetic overflow on signed shl in .*: FAILURE$
6+
^\[.*\] .* arithmetic overflow on signed shl in .*: FAILURE$
77
^\*\* 2 of 4 failed
88
^VERIFICATION FAILED$
99
--

regression/cbmc/Quantifiers-assertion/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] Exists-Exists: successful: SUCCESS$
6-
^\[main.assertion.2\] NotExists-NotExists: successful: SUCCESS$
7-
^\[main.assertion.3\] NotExists-Exists: failed: FAILURE$
8-
^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
9-
^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
10-
^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
5+
^\[main.assertion.1\] .* Exists-Exists: successful: SUCCESS$
6+
^\[main.assertion.2\] .* NotExists-NotExists: successful: SUCCESS$
7+
^\[main.assertion.3\] .* NotExists-Exists: failed: FAILURE$
8+
^\[main.assertion.4\] .* NotExists-Forall: failed: FAILURE$
9+
^\[main.assertion.5\] .* NotForall-Forall: successful: SUCCESS$
10+
^\[main.assertion.6\] .* NotForall-NotForall: successful: SUCCESS$
1111
^\*\* 2 of 6 failed
1212
^VERIFICATION FAILED$
1313
^EXIT=10$

regression/cbmc/Quantifiers-assignment/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ CORE
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] assertion x: SUCCESS$
6-
^\[main.assertion.2\] assertion y: FAILURE$
7-
^\[main.assertion.3\] assertion z1: SUCCESS$
8-
^\[main.assertion.4\] assertion z2: SUCCESS$
5+
^\[main.assertion.1\] .* assertion x: SUCCESS$
6+
^\[main.assertion.2\] .* assertion y: FAILURE$
7+
^\[main.assertion.3\] .* assertion z1: SUCCESS$
8+
^\[main.assertion.4\] .* assertion z2: SUCCESS$
99
^\*\* 1 of 4 failed
1010
^VERIFICATION FAILED$
1111
^EXIT=10$

0 commit comments

Comments
 (0)