Skip to content

Commit f1ba6fd

Browse files
NlightNFotisEnrico Steffinlongo
authored and
Enrico Steffinlongo
committed
Enable all shadow memory regression tests
1 parent 1c6defc commit f1ba6fd

File tree

32 files changed

+34
-30
lines changed

32 files changed

+34
-30
lines changed
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
---
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Start testing: Aug 09 16:45 BST
2+
----------------------------------------------------------
3+
End testing: Aug 09 16:45 BST

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)