Skip to content

Flip passing FUTURE tests to CORE in regression/cbmc-primitives #6438

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 4, 2021
Merged

Flip passing FUTURE tests to CORE in regression/cbmc-primitives #6438

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
FUTURE
CORE
main.c
--no-simplify --no-propagation
^EXIT=10$
Expand All @@ -10,5 +10,6 @@ main.c
--
Check that the dynamic object property is nondet for uninitialized pointers. We
use --no-simplify and --no-propagation to ensure that the case is not solved by
the constant propagation and thus tests the constraint encoding. Recorded as
ADA-526.
the constant propagation and thus tests the constraint encoding. We expect
that `__CPROVER_DYNAMIC_OBJECT` should be nondet for pointers that are neither
null nor valid.
3 changes: 1 addition & 2 deletions regression/cbmc-primitives/dynamic-object-02/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
FUTURE
CORE
main.c

^EXIT=10$
Expand All @@ -9,4 +9,3 @@ main.c
^warning: ignoring
--
Check that the dynamic object property is nondet for uninitialized pointers.
Recorded as ADA-526.
3 changes: 1 addition & 2 deletions regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
FUTURE
CORE
main.c
--no-simplify --no-propagation
^EXIT=10$
Expand All @@ -11,4 +11,3 @@ main.c
Check that both positive and negative offsets can be chosen for uninitialized
pointers. We use --no-simplify and --no-propagation to ensure that the case is
not solved by the constant propagation and thus tests the constraint encoding.
Recorded as ADA-528.
11 changes: 8 additions & 3 deletions regression/cbmc-primitives/pointer-offset-01/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
FUTURE
CORE
main.c

^EXIT=10$
Expand All @@ -8,5 +8,10 @@ main.c
--
^warning: ignoring
--
Check that both positive and negative offsets can be chosen for uninitialized
pointers. Recorded as ADA-528.
For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory
is allocated). Since the offset of pointers is signed, negative offsets should be
able to be chosen (along with positive ones) non-deterministically.
`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset
from the base address of the object. This test guards this, and especially
against the case where we could only observe some cases where offsets were only
positive (in some CI configurations, for instance).