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

src/ansi-c/cprover_builtin_headers.h

@@ -6,21 +6,26 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 void __CPROVER_havoc_object(void *);
 void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
-__CPROVER_bool __CPROVER_equal();
+#ifdef LIBRARY_CHECK 
+// __CPROVER_equal expects two arguments of the same type -- any type is
+// permitted, unsigned long long is just used for the benefit of running syntax
+// checks using system compilers
+__CPROVER_bool __CPROVER_equal(unsigned long long, unsigned long long);
+#endif
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 _Bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
-__CPROVER_bool __CPROVER_r_ok();
-__CPROVER_bool __CPROVER_w_ok();
-__CPROVER_bool __CPROVER_rw_ok();
+__CPROVER_bool __CPROVER_r_ok(void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_w_ok(void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_rw_ok(void *, __CPROVER_size_t);
 
 // experimental features for CHC encodings -- do not use
-__CPROVER_bool __CPROVER_is_list(); // a singly-linked null-terminated dynamically-allocated list
-__CPROVER_bool __CPROVER_is_dll();
-__CPROVER_bool __CPROVER_is_cyclic_dll();
-__CPROVER_bool __CPROVER_is_sentinel_dll();
+__CPROVER_bool __CPROVER_is_list(void *); // a singly-linked null-terminated dynamically-allocated list
+__CPROVER_bool __CPROVER_is_dll(void *);
+__CPROVER_bool __CPROVER_is_cyclic_dll(void *);
+__CPROVER_bool __CPROVER_is_sentinel_dll(void *);
 __CPROVER_bool __CPROVER_is_cstring(const char *);
 __CPROVER_size_t __CPROVER_cstrlen(const char *);
 __CPROVER_bool __CPROVER_separate(const void *, const void *, ...);
@@ -41,8 +46,8 @@ void __CPROVER_output(const char *id, ...);
 void __CPROVER_cover(__CPROVER_bool condition);
 
 // concurrency-related
-void __CPROVER_atomic_begin();
-void __CPROVER_atomic_end();
+void __CPROVER_atomic_begin(void);
+void __CPROVER_atomic_end(void);
 void __CPROVER_fence(const char *kind, ...);
 
 // contract-related functions
@@ -130,15 +135,23 @@ void __CPROVER_k_induction_hint(unsigned min, unsigned max,
 // format string-related
 int __CPROVER_scanf(const char *, ...);
 
+#ifdef LIBRARY_CHECK
+// The following built-ins are type checked by our C front-end and do not
+// require declarations. They work with any types as described below. unsigned
+// long long is just used to enable checks using system compilers.
 // detect overflow
-__CPROVER_bool __CPROVER_overflow_minus();
-__CPROVER_bool __CPROVER_overflow_mult();
-__CPROVER_bool __CPROVER_overflow_plus();
-__CPROVER_bool __CPROVER_overflow_shl();
-__CPROVER_bool __CPROVER_overflow_unary_minus();
+// the following expect two numeric arguments
+__CPROVER_bool __CPROVER_overflow_minus(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_mult(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_plus(unsigned long long, unsigned long long);
+__CPROVER_bool __CPROVER_overflow_shl(unsigned long long, unsigned long long);
+// expects one numeric argument
+__CPROVER_bool __CPROVER_overflow_unary_minus(unsigned long long);
 
 // enumerations
-__CPROVER_bool __CPROVER_enum_is_in_range();
+// expects one enum-typed argument
+__CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long);
+#endif
 
 // contracts
 void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,