Skip to content

Commit d9deb79

Browse files
committed
pointer encoding: tests changed
1 parent 913f7bf commit d9deb79

File tree

9 files changed

+9
-10
lines changed

9 files changed

+9
-10
lines changed

regression/cbmc-library/fprintf-01/test.desc

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

regression/cbmc-library/free-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--pointer-check --bounds-check --stop-on-fail
4-
free argument must be NULL or valid pointer
4+
free argument must be (dynamic object|NULL or valid pointer)
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

regression/cbmc/Pointer_comparison1/main.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,7 @@ int main()
1010
return 0;
1111

1212
if(
13-
(unsigned long)p >
14-
42) // unsoundly evaluates to true due to pointer encoding
13+
(unsigned long)p > 1) // unsoundly evaluates to true due to pointer encoding
1514
{
1615
return 0;
1716
}

regression/cbmc/address_space_size_limit1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE thorough-paths broken-smt-backend
1+
KNOWNBUG thorough-paths broken-smt-backend
22
test.c
33
--no-simplify --unwind 300 --object-bits 8
44
too many addressed objects

regression/cbmc/memory_allocation1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
KNOWNBUG broken-smt-backend
22
main.c
33
--pointer-check
44
^EXIT=10$

regression/cbmc/mm_io1/test.desc

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

44
^EXIT=0$

regression/cbmc/pointer-extra-checks/test.desc

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

regression/contracts/assigns-enforce-malloc-zero/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo _ --malloc-may-fail --malloc-fail-null
44
^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$

regression/contracts/test_struct_member_enforce/test.desc

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

0 commit comments

Comments
 (0)