replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

pointer expressions 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2386 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2013-04-14 18:52:14 +00:00
parent ac97bbf95e
commit b763fe46d6
3 changed files with 22 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/ansi-c/c_typecheck_expr.cpp
View File

@ -2068,7 +2068,20 @@ void c_typecheck_baset::do_special_functions(
throw "same_object expects two operands";
}
exprt same_object_expr("same-object", bool_typet());
predicate_exprt same_object_expr(ID_same_object);
same_object_expr.operands()=expr.arguments();
same_object_expr.location()=location;
expr.swap(same_object_expr);
}
else if(identifier==CPROVER_PREFIX "invalid_pointer")
{
if(expr.arguments().size()!=1)
{
err_location(f_op);
throw "invalid_pointer expects one operand";
}
predicate_exprt same_object_expr(ID_invalid_pointer);
same_object_expr.operands()=expr.arguments();
same_object_expr.location()=location;
expr.swap(same_object_expr);
@ -2094,7 +2107,7 @@ void c_typecheck_baset::do_special_functions(
throw "is_zero_string expects one operand";
}
exprt is_zero_string_expr("is_zero_string", bool_typet());
predicate_exprt is_zero_string_expr("is_zero_string");
is_zero_string_expr.operands()=expr.arguments();
is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
is_zero_string_expr.location()=location;

7
src/ansi-c/expr2c.cpp
View File

@ -3996,7 +3996,12 @@ std::string expr2ct::convert(
else if(src.id()==ID_same_object)
{
return convert_function(src, "SAME-OBJECT", precedence=16);
return convert_function(src, "__CPROVER_same_object", precedence=16);
}
else if(src.id()==ID_invalid_pointer)
{
return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
}
else if(src.id()==ID_dynamic_object)

1
src/ansi-c/internal_additions.cpp
View File

@ -93,6 +93,7 @@ void ansi_c_internal_additions(std::string &code)
"void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
"__CPROVER_bool __CPROVER_equal();\n"
"__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
"__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"
"__CPROVER_bool __CPROVER_is_zero_string(const void *);\n"
"__CPROVER_size_t __CPROVER_zero_string_length(const void *);\n"
"__CPROVER_size_t __CPROVER_buffer_size(const void *);\n"