Skip to content

Commit 01111ae

Browse files
committed
Enable all shadow memory regression tests
1 parent 5fb88ea commit 01111ae

File tree

30 files changed

+30
-30
lines changed

30 files changed

+30
-30
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-
FUTURE
1+
CORE
22
main.c
33

44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
main.c
33
--unwind 11
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-
FUTURE
1+
CORE
22
main.c
33
--unwind 11
44
^EXIT=0$

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

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

44
^EXIT=0$

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

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

44
^EXIT=0$

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

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

44
^EXIT=0$

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

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

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-
FUTURE
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-
FUTURE
1+
CORE
22
main.c
33

44
^EXIT=0$

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

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

44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
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-
FUTURE
1+
CORE
22
main.c
33

44
^EXIT=0$

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

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

44
^EXIT=0$

regression/cbmc-shadow-memory/no-shadow-memory-matching1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
main.c
33
--no-shadow-memory-matching '.*\.c:.*__cs_.*'
44
^EXIT=0$

regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
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-
FUTURE
1+
CORE
22
main.c
33

44
^EXIT=0$

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

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

44
^EXIT=0$

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

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

44
^EXIT=0$

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

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

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

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

44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
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-
FUTURE
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-
FUTURE
1+
CORE
22
main.c
33
--unwind 15
44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
FUTURE
1+
CORE
22
main.c
33
--stop-on-fail --unwind 5
44
^EXIT=10$

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-
FUTURE
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-
FUTURE
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-
FUTURE
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc-shadow-memory/var-assign1/test.desc

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

44
^EXIT=0$

regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc

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

44
^EXIT=6$

regression/cbmc-shadow-memory/void-ptr-param2/test.desc

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

44
^EXIT=0$

0 commit comments

Comments
 (0)