Skip to content

Commit 4655ef4

Browse files
NlightNFotisEnrico Steffinlongo
authored and
Enrico Steffinlongo
committed
Marking CORE more Shadow Memory regression tests
Marking as CORE all the shadow memory regression tests that are now passing. The remaining regression tests that are still marked as KNOWNBUG will be added as soon as the implementation will be fixed.
1 parent 1d4a8d1 commit 4655ef4

File tree

11 files changed

+11
-11
lines changed

11 files changed

+11
-11
lines changed

regression/cbmc-shadow-memory/char1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/constchar-pointers1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--unwind 11
44
^EXIT=0$

regression/cbmc-shadow-memory/linked-list1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/linked-list2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/maybe-null1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/struct-set1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/taint-example1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--unwind 15
44
^EXIT=0$

regression/cbmc-shadow-memory/union-get-max1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/union-get-or1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/union-set1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

0 commit comments

Comments
 (0)