Skip to content

Commit 43e4a83

Browse files
committed
Mark snapshot harness tests as KNOWNBUG for now.
1 parent bee9bb7 commit 43e4a83

File tree

26 files changed

+75
-25
lines changed

26 files changed

+75
-25
lines changed

regression/snapshot-harness/arrays_01/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -11,3 +11,5 @@ array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location
1111
VERIFICATION SUCCESSFUL
1212
--
1313
^warning: ignoring
14+
--
15+
For more information take a look at github#5351

regression/snapshot-harness/arrays_02/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -9,3 +9,5 @@ p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:
99
VERIFICATION SUCCESSFUL
1010
--
1111
^warning: ignoring
12+
--
13+
For more information take a look at github#5351

regression/snapshot-harness/dynamic-array-int-ordering/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=10$
@@ -14,3 +14,5 @@ a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type in
1414
VERIFICATION FAILED
1515
--
1616
unwinding assertion loop \d+: FAILURE
17+
--
18+
For more information take a look at github#5351

regression/snapshot-harness/dynamic-array-int/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=10$
@@ -16,3 +16,4 @@ VERIFICATION FAILED
1616
unwinding assertion loop \d+: FAILURE
1717
--
1818
Broken by https://github.com/diffblue/cbmc/issues/4978
19+
For more information take a look at github#5351

regression/snapshot-harness/function_pointer_01/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -9,3 +9,5 @@ fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location m
99
VERIFICATION SUCCESSFUL
1010
--
1111
^warning: ignoring
12+
--
13+
For more information take a look at github#5351

regression/snapshot-harness/function_pointer_02/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -11,3 +11,5 @@ fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-
1111
VERIFICATION SUCCESSFUL
1212
--
1313
^warning: ignoring
14+
--
15+
For more information take a look at github#5351

regression/snapshot-harness/function_pointer_03/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -11,3 +11,5 @@ fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --ini
1111
VERIFICATION SUCCESSFUL
1212
--
1313
^warning: ignoring
14+
--
15+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
44
^EXIT=0$
55
^SIGNAL=0$
66
VERIFICATION SUCCESSFUL
77
--
88
^warning: ignoring
9+
--
10+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL
77
--
88
unwinding assertion loop \d+: FAILURE
9+
--
10+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL
77
--
88
unwinding assertion loop \d+: FAILURE
9+
--
10+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL
77
--
88
unwinding assertion loop \d+: FAILURE
9+
--
10+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL
77
--
88
unwinding assertion loop \d+: FAILURE
9+
--
10+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -7,3 +7,5 @@ x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:
77
VERIFICATION SUCCESSFUL
88
--
99
^warning: ignoring
10+
--
11+
For more information take a look at github#5351

regression/snapshot-harness/pointer_02/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=10$
@@ -10,3 +10,5 @@ x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-locatio
1010
\[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS
1111
--
1212
^warning: ignoring
13+
--
14+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS
77
--
88
^warning: ignoring
9+
--
10+
For more information take a look at github#5351

regression/snapshot-harness/pointer_04/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -10,3 +10,5 @@ x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location m
1010
\[main.assertion.5\] line [0-9]+ assertion \*\*p2 == x: SUCCESS
1111
--
1212
^warning: ignoring
13+
--
14+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -7,3 +7,5 @@ x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location m
77
VERIFICATION SUCCESSFUL
88
--
99
^warning: ignoring
10+
--
11+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -7,3 +7,5 @@ p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:
77
VERIFICATION SUCCESSFUL
88
--
99
^warning: ignoring
10+
--
11+
For more information take a look at github#5351

regression/snapshot-harness/pointer_07/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=10$
@@ -9,3 +9,5 @@ p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
99
\[main.assertion.4\] line [0-9]+ assertion \*p1 != 1: SUCCESS
1010
--
1111
^warning: ignoring
12+
--
13+
For more information take a look at github#5351

regression/snapshot-harness/pointer_to_struct_01/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -10,3 +10,5 @@ st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location ma
1010
VERIFICATION SUCCESSFUL
1111
--
1212
^warning: ignoring
13+
--
14+
For more information take a look at github#5351

regression/snapshot-harness/simple-source-location/test.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
global_var --harness-type initialise-with-memory-snapshot --initial-source-location main.c:20
44
^EXIT=10$
@@ -10,3 +10,4 @@ VERIFICATION FAILED
1010
^warning: ignoring
1111
--
1212
The first assertion is succeeding because unreachable.
13+
For more information take a look at github#5351
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL
77
--
88
unwinding assertion loop \d+: FAILURE
9+
--
10+
For more information take a look at github#5351

regression/snapshot-harness/static-array-int/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,5 @@ array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initi
1111
VERIFICATION FAILED
1212
--
1313
unwinding assertion loop \d+: FAILURE
14+
--
15+
For more information take a look at github#5351

regression/snapshot-harness/structs_01/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -10,3 +10,5 @@ st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main
1010
VERIFICATION SUCCESSFUL
1111
--
1212
^warning: ignoring
13+
--
14+
For more information take a look at github#5351

regression/snapshot-harness/structs_02/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
st,p --harness-type initialise-with-memory-snapshot --initial-source-location main.c:27
44
^EXIT=0$
@@ -10,3 +10,5 @@ st,p --harness-type initialise-with-memory-snapshot --initial-source-location ma
1010
VERIFICATION SUCCESSFUL
1111
--
1212
^warning: ignoring
13+
--
14+
For more information take a look at github#5351

regression/snapshot-harness/union_01/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
un,ip,fp --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
44
^EXIT=0$
@@ -9,3 +9,5 @@ un,ip,fp --harness-type initialise-with-memory-snapshot --initial-goto-location
99
VERIFICATION SUCCESSFUL
1010
--
1111
^warning: ignoring
12+
--
13+
For more information take a look at github#5351

0 commit comments

Comments
 (0)