use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET

Author: kroening

doc/cbmc-user-manual.md

@@ -2193,8 +2193,8 @@ section on [Assumptions and Assertions](modeling-assertions.shtml).
 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
 
     _Bool __CPROVER_same_object(const void *, const void *);
-    unsigned __CPROVER_POINTER_OBJECT(const void *p);
-    signed __CPROVER_POINTER_OFFSET(const void *p);
+    __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
+    __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
     _Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
 
 The function **\_\_CPROVER\_same\_object** returns true if the two

src/ansi-c/ansi_c_internal_additions.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_internal_additions.h"
 
+#include <util/c_types.h>
 #include <util/config.h>
 
 #include <linking/static_lifetime_init.h>
@@ -126,6 +127,8 @@ void ansi_c_internal_additions(std::string &code)
   code+=
     "# 1 \"<built-in-additions>\"\n"
     "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n"
+    "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
+      " __CPROVER_ssize_t;\n"
     "const unsigned __CPROVER_constant_infinity_uint;\n"
     "typedef void __CPROVER_integer;\n"
     "typedef void __CPROVER_rational;\n"

src/ansi-c/c_typecheck_expr.cpp

@@ -2157,10 +2157,7 @@ exprt c_typecheck_baset::do_special_functions(
     exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
     pointer_offset_expr.add_source_location()=source_location;
 
-    if(expr.type()!=pointer_offset_expr.type())
-      pointer_offset_expr.make_typecast(expr.type());
-
-    return pointer_offset_expr;
+    return typecast_exprt::conditional_cast(pointer_offset_expr, expr.type());
   }
   else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
   {
@@ -2171,11 +2168,10 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt pointer_object_expr=exprt(ID_pointer_object, expr.type());
-    pointer_object_expr.operands()=expr.arguments();
-    pointer_object_expr.add_source_location()=source_location;
+    exprt pointer_object_expr = pointer_object(expr.arguments().front());
+    pointer_object_expr.add_source_location() = source_location;
 
-    return pointer_object_expr;
+    return typecast_exprt::conditional_cast(pointer_object_expr, expr.type());
   }
   else if(identifier=="__builtin_bswap16" ||
           identifier=="__builtin_bswap32" ||

src/ansi-c/cprover_builtin_headers.h

@@ -33,9 +33,9 @@ void __CPROVER_fence(const char *kind, ...);
 void CBMC_trace(int lvl, const char *event, ...);
 
 // pointers
-unsigned __CPROVER_POINTER_OBJECT(const void *p);
-signed __CPROVER_POINTER_OFFSET(const void *p);
-__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
+__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
+__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
+__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
 void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
 
 // float stuff

src/cpp/cpp_internal_additions.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include <util/c_types.h>
 #include <util/config.h>
 
 #include <ansi-c/ansi_c_internal_additions.h>
@@ -64,7 +65,11 @@ void cpp_internal_additions(std::ostream &out)
 
   // types
   out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n';
-  out << "typedef __typeof__(sizeof(int)) __CPROVER_size_t;" << '\n';
+  out << "typedef __CPROVER::size_t __CPROVER_size_t;" << '\n';
+  out << "typedef "
+      << c_type_as_string(signed_size_type().get(ID_C_c_type))
+      << " __CPROVER::ssize_t;" << '\n';
+  out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n';
 
   // assume/assert
   out << "extern \"C\" void assert(bool assertion);" << '\n';
@@ -85,8 +90,8 @@ void cpp_internal_additions(std::ostream &out)
   out << "extern \"C\" void __CPROVER::atomic_end();" << '\n';
 
   // pointers
-  out << "extern \"C\" unsigned __CPROVER_POINTER_OBJECT(const void *p);\n";
-  out << "extern \"C\" signed __CPROVER_POINTER_OFFSET(const void *p);" << '\n';
+  out << "extern \"C\" __CPROVER::size_t __CPROVER_POINTER_OBJECT(const void *);\n";
+  out << "extern \"C\" __CPROVER::ssize_t __CPROVER_POINTER_OFFSET(const void *);" << '\n';
   out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n';
   // NOLINTNEXTLINE(whitespace/line_length)
   out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';

src/util/pointer_predicates.h

@@ -17,38 +17,39 @@ class namespacet;
 class typet;
 
 exprt same_object(const exprt &p1, const exprt &p2);
-exprt deallocated(const exprt &pointer, const namespacet &ns);
-exprt dead_object(const exprt &pointer, const namespacet &ns);
-exprt dynamic_size(const namespacet &ns);
+exprt deallocated(const exprt &pointer, const namespacet &);
+exprt dead_object(const exprt &pointer, const namespacet &);
+exprt dynamic_size(const namespacet &);
 exprt pointer_offset(const exprt &pointer);
-exprt malloc_object(const exprt &pointer, const namespacet &ns);
+exprt pointer_object(const exprt &pointer);
+exprt malloc_object(const exprt &pointer, const namespacet &);
 exprt object_size(const exprt &pointer);
 exprt pointer_object_has_type(
-  const exprt &pointer, const typet &type, const namespacet &ns);
+  const exprt &pointer, const typet &type, const namespacet &);
 exprt dynamic_object(const exprt &pointer);
 exprt good_pointer(const exprt &pointer);
-exprt good_pointer_def(const exprt &pointer, const namespacet &ns);
+exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);
 exprt null_pointer(const exprt &pointer);
 exprt integer_address(const exprt &pointer);
 exprt invalid_pointer(const exprt &pointer);
 exprt dynamic_object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
+  const namespacet &,
   const exprt &offset);
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
   const typet &dereference_type,
-  const namespacet &ns,
+  const namespacet &,
   const exprt &access_size);
 exprt object_lower_bound(
   const exprt &pointer,
-  const namespacet &ns,
+  const namespacet &,
   const exprt &offset);
 exprt object_upper_bound(
   const exprt &pointer,
   const typet &dereference_type,
-  const namespacet &ns,
+  const namespacet &,
   const exprt &access_size);
 
 #endif // CPROVER_UTIL_POINTER_PREDICATES_H