Mark snapshot tests as KNOWNBUG

NlightNFotis · NlightNFotis · commit aa640fd05eae · 2020-05-22T10:10:04.000+01:00
The C output doesn't quite work with the snapshot harness at the moment
(specifically, it doesn't work with the feature to restart analysis from
a specific point in the program) so these test are marked as KNOWNBUG
for now.

Going forward we may re-enable these after fixing the feature, or
possibly do without the restarting entirely.
diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
@@ -7,3 +7,5 @@ main.c
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/havoc-global-int-03/test.desc b/regression/goto-harness/havoc-global-int-03/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
 ^EXIT=10$
@@ -8,3 +8,5 @@ main.c
 \[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
 ^EXIT=10$
diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=10$
@@ -7,3 +7,5 @@ main.c
 \[main.assertion.2\] line [0-9]+ assertion y == 1: FAILURE
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+More information can be found in github#5351.
diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
diff --git a/regression/snapshot-harness/arrays_01/test.desc b/regression/snapshot-harness/arrays_01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/arrays_02/test.desc b/regression/snapshot-harness/arrays_02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -9,3 +9,5 @@ p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc b/regression/snapshot-harness/dynamic-array-int-ordering/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -14,3 +14,5 @@ a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type in
 VERIFICATION FAILED
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/dynamic-array-int/test.desc b/regression/snapshot-harness/dynamic-array-int/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -16,3 +16,4 @@ VERIFICATION FAILED
 unwinding assertion loop \d+: FAILURE
 --
 Broken by https://github.com/diffblue/cbmc/issues/4978
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/function_pointer_01/test.desc b/regression/snapshot-harness/function_pointer_01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -9,3 +9,5 @@ fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location m
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/function_pointer_02/test.desc b/regression/snapshot-harness/function_pointer_02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/function_pointer_03/test.desc b/regression/snapshot-harness/function_pointer_03/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -11,3 +11,5 @@ fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --ini
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc b/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 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
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 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
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer-to-array-char/test.desc b/regression/snapshot-harness/pointer-to-array-char/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 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
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer-to-array-int/test.desc b/regression/snapshot-harness/pointer-to-array-int/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 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
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_01/test.desc b/regression/snapshot-harness/pointer_01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -7,3 +7,5 @@ x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_02/test.desc b/regression/snapshot-harness/pointer_02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -10,3 +10,5 @@ x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-locatio
 \[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_03/test.desc b/regression/snapshot-harness/pointer_03/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_04/test.desc b/regression/snapshot-harness/pointer_04/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -10,3 +10,5 @@ x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location m
 \[main.assertion.5\] line [0-9]+ assertion \*\*p2 == x: SUCCESS
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_05/test.desc b/regression/snapshot-harness/pointer_05/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -7,3 +7,5 @@ x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location m
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_06/test.desc b/regression/snapshot-harness/pointer_06/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -7,3 +7,5 @@ p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_07/test.desc b/regression/snapshot-harness/pointer_07/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -9,3 +9,5 @@ p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 \[main.assertion.4\] line [0-9]+ assertion \*p1 != 1: SUCCESS
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/pointer_to_struct_01/test.desc b/regression/snapshot-harness/pointer_to_struct_01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -10,3 +10,5 @@ st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location ma
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/simple-source-location/test.desc b/regression/snapshot-harness/simple-source-location/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 global_var --harness-type initialise-with-memory-snapshot --initial-source-location main.c:20
 ^EXIT=10$
@@ -10,3 +10,4 @@ VERIFICATION FAILED
 ^warning: ignoring
 --
 The first assertion is succeeding because unreachable.
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/static-array-char/test.desc b/regression/snapshot-harness/static-array-char/test.desc
@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/static-array-int/test.desc b/regression/snapshot-harness/static-array-int/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
@@ -11,3 +11,5 @@ array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initi
 VERIFICATION FAILED
 --
 unwinding assertion loop \d+: FAILURE
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/structs_01/test.desc b/regression/snapshot-harness/structs_01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
@@ -10,3 +10,5 @@ st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/structs_02/test.desc b/regression/snapshot-harness/structs_02/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 st,p --harness-type initialise-with-memory-snapshot --initial-source-location main.c:27
 ^EXIT=0$
@@ -10,3 +10,5 @@ st,p --harness-type initialise-with-memory-snapshot --initial-source-location ma
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
+--
+For more information take a look at github#5351
diff --git a/regression/snapshot-harness/union_01/test.desc b/regression/snapshot-harness/union_01/test.desc

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`main.c`
`3`	`3`	`--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple`
`4`	`4`	`^EXIT=10$`