Make CPROVER intrinsics proper prototypes

Forward declarations without arguments are deprecated in C. Polymorphic
built-ins now have dummy declarations that are only in effect when
running library checks. Our own C front-end will type check them
properly and won't rely on forward declarations.

Author: tautschnig

doc/cprover-manual/api.md

@@ -191,11 +191,8 @@ option to verify the preconditions of the primitives.
 ```C
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p);
 _Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
-void __CPROVER_r_ok(const T *p);
 void __CPROVER_r_ok(const void *p, size_t size);
-void __CPROVER_w_ok(const T *p);
 void __CPROVER_w_ok(const void *p, size_t size);
-void __CPROVER_rw_ok(const T *p);
 void __CPROVER_rw_ok(const void *p, size_t size);
 ```
 
@@ -207,9 +204,7 @@ object.
 The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
 memory starting at the given pointer with the given size is safe. 
 **\_\_CPROVER\_w_ok** does the same with writing, and **\_\_CPROVER\_rw_ok**
-returns true when it is safe to do both.  These predicates can be given an
-optional size; when the size argument is not given, the size of the subtype
-(which must not be **void**) of the pointer type is used.
+returns true when it is safe to do both.
 
 #### \_\_CPROVER\_havoc\_object
 

regression/cbmc/pointer-predicates/at_bounds1.c

@@ -9,7 +9,7 @@ int main()
   if(p != NULL && s != __CPROVER_max_malloc_size)
   {
     char *q = p + s;
-    __CPROVER_assert(__CPROVER_r_ok(q, 0), "should be valid");
-    __CPROVER_assert(!__CPROVER_r_ok(q + 1, 0), "should fail");
+    __CPROVER_assert(__CPROVER_r_ok(q, 0ull), "should be valid");
+    __CPROVER_assert(!__CPROVER_r_ok(q + 1, 0ull), "should fail");
   }
 }

regression/cbmc/pointer-predicates/at_bounds1.desc

@@ -1,7 +1,7 @@
 CORE broken-smt-backend new-smt-backend
 at_bounds1.c
 --pointer-primitive-check --malloc-fail-null
-^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(\(const void \*\)\(q \+ (\(signed (long (long )?)?int\))?1\), 0ull\): FAILURE$
 ^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/pointer-primitive-check-01/main.c

@@ -18,10 +18,10 @@ void main()
   __CPROVER_OBJECT_SIZE(p4);
 
   char *p5;
-  __CPROVER_r_ok(p5, 1);
+  __CPROVER_r_ok(p5, 1ull);
 
   char *p6;
-  __CPROVER_w_ok(p6, 1);
+  __CPROVER_w_ok(p6, 1ull);
 
   char *p7;
   __CPROVER_DYNAMIC_OBJECT(p7);

regression/cbmc/pointer-primitive-check-01/test.desc

@@ -7,14 +7,14 @@ main.c
 \[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
-\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
-\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
-\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
-\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, 1ull\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, 1ull\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(\(const void \*\)p5, 1ull\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, 1ull\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, 1ull\): FAILURE
+\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, 1ull\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(\(const void \*\)p6, 1ull\): SUCCESS
+\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, 1ull\): FAILURE
 \[main.pointer_primitives.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
 \[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
 \[main.pointer_primitives.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS

regression/cbmc/pointer-primitive-check-04/test.desc

@@ -3,10 +3,10 @@ main.c
 --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(p, .*1\): FAILURE
-\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(p, .*1\): SUCCESS
-\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(p, .*1\): SUCCESS
-\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(p, .*1\): FAILURE
+\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, .*1\): FAILURE
+\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, .*1\): SUCCESS
+\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, .*1\): SUCCESS
+\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, .*1\): FAILURE
 --
 ^warning: ignoring
 --

regression/cbmc/pragma_cprover3/main.c

@@ -20,7 +20,7 @@ int main()
   }
 
   // generate check and fail on the following statements
-  if(__CPROVER_r_ok(q, 1))
+  if(__CPROVER_r_ok(q, 1ull))
   {
   }
 }

regression/cbmc/pragma_cprover3/test.desc

@@ -2,8 +2,8 @@ CORE new-smt-backend
 main.c
 --pointer-primitive-check
 ^main.c function main$
-^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/pragma_cprover_enable3/main.c

@@ -5,13 +5,13 @@ int main()
 #pragma CPROVER check push
 #pragma CPROVER check enable "pointer-primitive"
   // generate checks for the following statements and fail
-  if(__CPROVER_r_ok(p, 1))
+  if(__CPROVER_r_ok(p, 1ull))
   {
   }
 #pragma CPROVER check pop
 
   // but do not generate checks on the following statements
-  if(__CPROVER_r_ok(q, 1))
+  if(__CPROVER_r_ok(q, 1ull))
   {
   }
 }

regression/cbmc/pragma_cprover_enable3/test.desc

@@ -2,8 +2,8 @@ CORE new-smt-backend
 main.c
 
 ^main.c function main$
-^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
+^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$