Merge pull request #7454 from qinheping/expr2c

Add CPROVER prefix to memory primitives produced by expr2c

Author: tautschnig

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.

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$

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$
 --

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$

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$

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`.
 

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).

src/ansi-c/expr2c.cpp

@@ -4012,9 +4012,10 @@ optionalt<std::string> 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"},