From 1a7235defdfbbec0eec8528015b197fb444dbdcb Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 20:30:24 +0100 Subject: [PATCH] use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET --- doc/cbmc-user-manual.md | 4 ++-- src/ansi-c/ansi_c_internal_additions.cpp | 3 +++ src/ansi-c/c_typecheck_expr.cpp | 12 ++++-------- src/ansi-c/cprover_builtin_headers.h | 6 +++--- src/cpp/cpp_internal_additions.cpp | 11 ++++++++--- src/util/pointer_predicates.h | 21 +++++++++++---------- 6 files changed, 31 insertions(+), 26 deletions(-) diff --git a/doc/cbmc-user-manual.md b/doc/cbmc-user-manual.md index e23aff11df9..94b27408feb 100644 --- a/doc/cbmc-user-manual.md +++ b/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 diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index d488b31f14f..54b81ce6efe 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_internal_additions.h" +#include #include #include @@ -126,6 +127,8 @@ void ansi_c_internal_additions(std::string &code) code+= "# 1 \"\"\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" diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index d31c7d242de..f78db70d7d7 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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" || diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 48b0d056b14..0b05aa245e7 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/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 diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 85363a59b69..2c3d33a00d6 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include @@ -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'; diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index 201d094f50a..ca149cfbc83 100644 --- a/src/util/pointer_predicates.h +++ b/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