Skip to content

use __CPROVER_s/size_t for __CPROVER_POINTER_OBJECT/OFFSET #2229

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 29, 2018
Merged

use __CPROVER_s/size_t for __CPROVER_POINTER_OBJECT/OFFSET #2229

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions doc/cbmc-user-manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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"
Expand Down
12 changes: 4 additions & 8 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")
{
Expand All @@ -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" ||
Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/cprover_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
11 changes: 8 additions & 3 deletions src/cpp/cpp_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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';
Expand All @@ -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';
Expand Down
21 changes: 11 additions & 10 deletions src/util/pointer_predicates.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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