cprover
pointer_predicates.h File Reference

Various predicates over pointers in programs. More...

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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 pointer_offset (const exprt &pointer)
 
exprt malloc_object (const exprt &pointer, const namespacet &ns)
 
exprt object_size (const exprt &pointer)
 
exprt pointer_object_has_type (const exprt &pointer, const typet &type, const namespacet &ns)
 
exprt dynamic_object (const exprt &pointer)
 
exprt good_pointer (const exprt &pointer)
 
exprt good_pointer_def (const exprt &pointer, const namespacet &ns)
 
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 exprt &offset)
 
exprt dynamic_object_upper_bound (const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
 
exprt object_lower_bound (const exprt &pointer, const namespacet &ns, const exprt &offset)
 
exprt object_upper_bound (const exprt &pointer, const typet &dereference_type, const namespacet &ns, const exprt &access_size)
 

Detailed Description

Various predicates over pointers in programs.

Definition in file pointer_predicates.h.

Function Documentation

§ dead_object()

exprt dead_object ( const exprt pointer,
const namespacet ns 
)

§ deallocated()

§ dynamic_object()

§ dynamic_object_lower_bound()

exprt dynamic_object_lower_bound ( const exprt pointer,
const namespacet ns,
const exprt offset 
)

§ dynamic_object_upper_bound()

exprt dynamic_object_upper_bound ( const exprt pointer,
const typet dereference_type,
const namespacet ns,
const exprt access_size 
)

§ dynamic_size()

exprt dynamic_size ( const namespacet ns)

§ good_pointer()

exprt good_pointer ( const exprt pointer)

Definition at line 85 of file pointer_predicates.cpp.

§ good_pointer_def()

§ integer_address()

exprt integer_address ( const exprt pointer)

Definition at line 152 of file pointer_predicates.cpp.

References null_pointer(), same_object(), to_pointer_type(), and exprt::type().

Referenced by mm_io().

§ invalid_pointer()

exprt invalid_pointer ( const exprt pointer)

§ malloc_object()

§ null_object()

exprt null_object ( const exprt pointer)

§ null_pointer()

§ object_lower_bound()

exprt object_lower_bound ( const exprt pointer,
const namespacet ns,
const exprt offset 
)

§ object_size()

§ object_upper_bound()

exprt object_upper_bound ( const exprt pointer,
const typet dereference_type,
const namespacet ns,
const exprt access_size 
)

§ pointer_object_has_type()

exprt pointer_object_has_type ( const exprt pointer,
const typet type,
const namespacet ns 
)

§ pointer_offset()

§ same_object()