__CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end
This commit is contained in:
parent
0618f7d30a
commit
acfea65cba
|
@ -2190,6 +2190,15 @@ to the program. If the expression evaluates to false, the execution
|
|||
aborts without failure. More detail on the use of assumptions is in the
|
||||
section on [Assumptions and Assertions](modeling-assertions.shtml).
|
||||
|
||||
#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
|
||||
|
||||
void __CPROVER_r_ok(const void *, size_t size);
|
||||
void __CPROVER_w_ok(cosnt void *, size_t size);
|
||||
|
||||
The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
|
||||
memory starting at the given pointer with the given size is safe.
|
||||
**\_\_CPROVER\_w_ok** does the same with writing.
|
||||
|
||||
#### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
|
||||
|
||||
_Bool __CPROVER_same_object(const void *, const void *);
|
||||
|
|
|
@ -2334,6 +2334,23 @@ exprt c_typecheck_baset::do_special_functions(
|
|||
|
||||
return malloc_expr;
|
||||
}
|
||||
else if(
|
||||
identifier == CPROVER_PREFIX "r_ok" || identifier == CPROVER_PREFIX "w_ok")
|
||||
{
|
||||
if(expr.arguments().size() != 2)
|
||||
{
|
||||
err_location(f_op);
|
||||
error() << identifier << " expects two operands" << eom;
|
||||
throw 0;
|
||||
}
|
||||
|
||||
irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
|
||||
|
||||
predicate_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
|
||||
ok_expr.add_source_location() = source_location;
|
||||
|
||||
return ok_expr;
|
||||
}
|
||||
else if(identifier==CPROVER_PREFIX "isinff" ||
|
||||
identifier==CPROVER_PREFIX "isinfd" ||
|
||||
identifier==CPROVER_PREFIX "isinfld" ||
|
||||
|
|
|
@ -9,6 +9,8 @@ __CPROVER_bool __CPROVER_invalid_pointer(const void *);
|
|||
__CPROVER_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(const void *, __CPROVER_size_t);
|
||||
__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
|
||||
|
||||
// bitvector analysis
|
||||
__CPROVER_bool __CPROVER_get_flag(const void *, const char *);
|
||||
|
|
|
@ -3515,6 +3515,12 @@ std::string expr2ct::convert_with_precedence(
|
|||
return convert_function(src, "__builtin_popcount", precedence=16);
|
||||
}
|
||||
|
||||
else if(src.id() == ID_r_ok)
|
||||
return convert_function(src, "R_OK", precedence = 16);
|
||||
|
||||
else if(src.id() == ID_w_ok)
|
||||
return convert_function(src, "W_OK", precedence = 16);
|
||||
|
||||
else if(src.id()==ID_invalid_pointer)
|
||||
return convert_function(src, "INVALID-POINTER", precedence=16);
|
||||
|
||||
|
|
|
@ -24,6 +24,8 @@ void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
|
|||
__CPROVER_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(const void *, __CPROVER_size_t);
|
||||
__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
|
||||
|
||||
#if 0
|
||||
__CPROVER_bool __CPROVER_equal();
|
||||
|
|
|
@ -691,6 +691,8 @@ IREP_ID_TWO(C_unnamed_object, #unnamed_object)
|
|||
IREP_ID_TWO(C_temporary_avoided, #temporary_avoided)
|
||||
IREP_ID_TWO(C_qualifier, #qualifier)
|
||||
IREP_ID_TWO(C_array_ini, #array_ini)
|
||||
IREP_ID_ONE(r_ok)
|
||||
IREP_ID_ONE(w_ok)
|
||||
|
||||
// Projects depending on this code base that wish to extend the list of
|
||||
// available ids should provide a file local_irep_ids.def in their source tree
|
||||
|
|
Loading…
Reference in New Issue