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 &)
 
exprt dead_object (const exprt &pointer, const namespacet &)
 
exprt dynamic_size (const namespacet &)
 
exprt pointer_offset (const exprt &pointer)
 
exprt pointer_object (const exprt &pointer)
 
exprt malloc_object (const exprt &pointer, const namespacet &)
 
exprt object_size (const exprt &pointer)
 
exprt dynamic_object (const exprt &pointer)
 
exprt good_pointer (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 integer_address (const exprt &pointer)
 
exprt invalid_pointer (const exprt &pointer)
 
exprt dynamic_object_lower_bound (const exprt &pointer, const namespacet &, const exprt &offset)
 
exprt dynamic_object_upper_bound (const exprt &pointer, const namespacet &, const exprt &access_size)
 
exprt object_lower_bound (const exprt &pointer, const namespacet &, const exprt &offset)
 
exprt object_upper_bound (const exprt &pointer, const namespacet &, 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  
)

Definition at line 58 of file pointer_predicates.cpp.

◆ deallocated()

exprt deallocated ( const exprt pointer,
const namespacet  
)

Definition at line 50 of file pointer_predicates.cpp.

◆ dynamic_object()

exprt dynamic_object ( const exprt pointer)

Definition at line 71 of file pointer_predicates.cpp.

◆ dynamic_object_lower_bound()

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

Definition at line 146 of file pointer_predicates.cpp.

◆ dynamic_object_upper_bound()

exprt dynamic_object_upper_bound ( const exprt pointer,
const namespacet ,
const exprt access_size 
)

Definition at line 154 of file pointer_predicates.cpp.

◆ dynamic_size()

exprt dynamic_size ( const namespacet )

Definition at line 66 of file pointer_predicates.cpp.

◆ good_pointer()

exprt good_pointer ( const exprt pointer)

Definition at line 78 of file pointer_predicates.cpp.

◆ good_pointer_def()

exprt good_pointer_def ( const exprt pointer,
const namespacet  
)

Definition at line 83 of file pointer_predicates.cpp.

◆ integer_address()

exprt integer_address ( const exprt pointer)

Definition at line 128 of file pointer_predicates.cpp.

◆ invalid_pointer()

exprt invalid_pointer ( const exprt pointer)

Definition at line 141 of file pointer_predicates.cpp.

◆ malloc_object()

exprt malloc_object ( const exprt pointer,
const namespacet  
)

Definition at line 42 of file pointer_predicates.cpp.

◆ null_object()

exprt null_object ( const exprt pointer)

Definition at line 122 of file pointer_predicates.cpp.

◆ null_pointer()

exprt null_pointer ( const exprt pointer)

Definition at line 135 of file pointer_predicates.cpp.

◆ object_lower_bound()

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

Definition at line 221 of file pointer_predicates.cpp.

◆ object_size()

exprt object_size ( const exprt pointer)

Definition at line 32 of file pointer_predicates.cpp.

◆ object_upper_bound()

exprt object_upper_bound ( const exprt pointer,
const namespacet ,
const exprt access_size 
)

Definition at line 187 of file pointer_predicates.cpp.

◆ pointer_object()

exprt pointer_object ( const exprt pointer)

Definition at line 22 of file pointer_predicates.cpp.

◆ pointer_offset()

exprt pointer_offset ( const exprt pointer)

Definition at line 37 of file pointer_predicates.cpp.

◆ same_object()

exprt same_object ( const exprt p1,
const exprt p2 
)

Definition at line 27 of file pointer_predicates.cpp.