diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index 112f69b7437..fb52df0c4de 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -3,10 +3,10 @@ main.c --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -\[main.pointer_primitives.\d+\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE -\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS -\[main.pointer_primitives.\d+\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS -\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ pointer invalid in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ dead object in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): FAILURE \[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE \[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS \[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS @@ -21,18 +21,18 @@ main.c \[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE -- ^warning: ignoring -\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE -\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE -\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE -\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE -\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE -\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS -\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in __CPROVER_POINTER_OBJECT\(\(const void \*\)p1\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in __CPROVER_POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in __CPROVER_POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in __CPROVER_POINTER_OBJECT\(\(const void \*\)p1\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in __CPROVER_POINTER_OFFSET\(\(const void \*\)p2\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in __CPROVER_POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in __CPROVER_POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in __CPROVER_POINTER_OFFSET\(\(const void \*\)p2\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in __CPROVER_POINTER_OBJECT\(\(const void \*\)p3\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in __CPROVER_POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in __CPROVER_POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in __CPROVER_POINTER_OBJECT\(\(const void \*\)p3\): FAILURE -- Verifies that checks are added for exactly those pointer primitives that are not universally well defined. diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index f1fc63f61ec..09560eaedd6 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -2,15 +2,15 @@ CORE main.c --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check ^\[foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$ -^\[foo.assigns.\d+\] line 11 Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 11 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$ ^\[bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$ ^\[bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$ -^\[bar.assigns.\d+\] line 19 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line 19 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ ^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$ ^\[baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$ -^\[baz.assigns.\d+\] line 25 Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ +^\[baz.assigns.\d+\] line 25 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ ^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc index f7d805e7c2a..440e688a534 100644 --- a/regression/contracts/assigns_enforce_20/test.desc +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ ^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc index 7476de365ce..e8150f13152 100644 --- a/regression/contracts/assigns_enforce_arrays_02/test.desc +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -7,7 +7,7 @@ main.c ^\[f2.assigns.\d+\] line 12 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid: SUCCESS$ ^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$ ^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$ -^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line 16 Check that __CPROVER_POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_conditional_unions/test.desc b/regression/contracts/assigns_enforce_conditional_unions/test.desc index 2e5c41421aa..04637c10efe 100644 --- a/regression/contracts/assigns_enforce_conditional_unions/test.desc +++ b/regression/contracts/assigns_enforce_conditional_unions/test.desc @@ -7,15 +7,15 @@ main.c ^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS ^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$ ^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 84 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$ ^\[update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$ +^\[update.assigns.\d+\] line 90 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$ ^\[update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 95 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ ^\[update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ -^\[update.assigns.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 100 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$ ^\[update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ -^\[update.assigns.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[update.assigns.\d+\] line 104 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ ^\[update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 6331637168a..3bc041ab15c 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -10,7 +10,7 @@ main.c ^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ @@ -19,7 +19,7 @@ main.c ^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: FAILURE$ ^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: FAILURE$ ^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ -- Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc index 1ef1d909911..2563aafae1a 100644 --- a/regression/contracts/assigns_enforce_havoc_object/test.desc +++ b/regression/contracts/assigns_enforce_havoc_object/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ +^\[bar.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- -Checks that __CPROVER_havoc_object(x) is detected as a write to POINTER_OBJECT(x). +Checks that __CPROVER_havoc_object(x) is detected as a write to __CPROVER_POINTER_OBJECT(x). diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index b6a434d4d7d..8fcf2b57224 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -4012,9 +4012,10 @@ optionalt expr2ct::convert_function(const exprt &src) {ID_isinf, "isinf"}, {ID_isnan, "isnan"}, {ID_isnormal, "isnormal"}, - {ID_object_size, "OBJECT_SIZE"}, - {ID_pointer_object, "POINTER_OBJECT"}, - {ID_pointer_offset, "POINTER_OFFSET"}, + {ID_object_size, CPROVER_PREFIX "OBJECT_SIZE"}, + {ID_pointer_object, CPROVER_PREFIX "POINTER_OBJECT"}, + {ID_pointer_offset, CPROVER_PREFIX "POINTER_OFFSET"}, + {ID_loop_entry, CPROVER_PREFIX "loop_entry"}, {ID_saturating_minus, CPROVER_PREFIX "saturating_minus"}, {ID_saturating_plus, CPROVER_PREFIX "saturating_plus"}, {ID_r_ok, "R_OK"},