cprover
Loading...
Searching...
No Matches
pointer_predicates.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Various predicates over pointers in programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_UTIL_POINTER_PREDICATES_H
13#define CPROVER_UTIL_POINTER_PREDICATES_H
14
15#include "deprecate.h"
16#include "std_expr.h"
17
18#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
19
20exprt same_object(const exprt &p1, const exprt &p2);
21exprt deallocated(const exprt &pointer, const namespacet &);
22exprt dead_object(const exprt &pointer, const namespacet &);
23exprt pointer_offset(const exprt &pointer);
24exprt pointer_object(const exprt &pointer);
25exprt object_size(const exprt &pointer);
26DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
27exprt dynamic_object(const exprt &pointer);
28exprt good_pointer(const exprt &pointer);
29exprt good_pointer_def(const exprt &pointer, const namespacet &);
30exprt null_object(const exprt &pointer);
31exprt null_pointer(const exprt &pointer);
32exprt integer_address(const exprt &pointer);
34 const exprt &pointer,
35 const exprt &offset);
37 const exprt &pointer,
38 const exprt &access_size);
39
48
49template <>
51{
52 return base.id() == ID_is_invalid_pointer;
53}
54
55inline void validate_expr(const is_invalid_pointer_exprt &value)
56{
57 validate_operands(value, 1, "is_invalid_pointer must have one operand");
58}
59
60#endif // CPROVER_UTIL_POINTER_PREDICATES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
const irep_idt & id() const
Definition irep.h:396
is_invalid_pointer_exprt(exprt pointer)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:495
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
STL namespace.
exprt pointer_offset(const exprt &pointer)
exprt integer_address(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt dead_object(const exprt &pointer, const namespacet &)
exprt object_upper_bound(const exprt &pointer, const exprt &access_size)
void validate_expr(const is_invalid_pointer_exprt &value)
exprt good_pointer(const exprt &pointer)
exprt deallocated(const exprt &pointer, const namespacet &)
exprt same_object(const exprt &p1, const exprt &p2)
exprt dynamic_object(const exprt &pointer)
bool can_cast_expr< is_invalid_pointer_exprt >(const exprt &base)
exprt pointer_object(const exprt &pointer)
exprt good_pointer_def(const exprt &pointer, const namespacet &)
exprt null_object(const exprt &pointer)
exprt null_pointer(const exprt &pointer)
exprt object_lower_bound(const exprt &pointer, const exprt &offset)
API to expression classes.