#include "std_expr.h"

Include dependency graph for pointer_predicates.h:

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

Classes
class	is_invalid_pointer_exprt

Macros
#define	SYMEX_DYNAMIC_PREFIX "symex_dynamic::"

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	pointer_offset (const exprt &pointer)

exprt	pointer_object (const exprt &pointer)

exprt	object_size (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	object_lower_bound (const exprt &pointer, const exprt &offset)

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

template<>
bool	can_cast_expr< is_invalid_pointer_exprt > (const exprt &base)

void	validate_expr (const is_invalid_pointer_exprt &value)

Detailed Description

Various predicates over pointers in programs

Definition in file pointer_predicates.h.

Macro Definition Documentation

◆ SYMEX_DYNAMIC_PREFIX

#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"

Definition at line 17 of file pointer_predicates.h.

Function Documentation

◆ can_cast_expr< is_invalid_pointer_exprt >()

template<>

bool can_cast_expr< is_invalid_pointer_exprt > ( const exprt & base )

inline

Definition at line 47 of file pointer_predicates.h.

◆ dead_object()

exprt dead_object	(	const exprt &	pointer,
		const namespacet &
	)

Definition at line 51 of file pointer_predicates.cpp.

◆ deallocated()

exprt deallocated	(	const exprt &	pointer,
		const namespacet &
	)

Definition at line 43 of file pointer_predicates.cpp.

◆ good_pointer()

exprt good_pointer ( const exprt & pointer )

Definition at line 59 of file pointer_predicates.cpp.

◆ good_pointer_def()

exprt good_pointer_def	(	const exprt &	pointer,
		const namespacet &
	)

Definition at line 64 of file pointer_predicates.cpp.

◆ integer_address()

exprt integer_address ( const exprt & pointer )

Definition at line 93 of file pointer_predicates.cpp.

◆ null_object()

exprt null_object ( const exprt & pointer )

Definition at line 87 of file pointer_predicates.cpp.

◆ null_pointer()

exprt null_pointer ( const exprt & pointer )

Definition at line 100 of file pointer_predicates.cpp.

◆ object_lower_bound()

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

Definition at line 136 of file pointer_predicates.cpp.

◆ object_size()

exprt object_size ( const exprt & pointer )

Definition at line 33 of file pointer_predicates.cpp.

◆ object_upper_bound()

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

Definition at line 106 of file pointer_predicates.cpp.

◆ pointer_object()

exprt pointer_object ( const exprt & pointer )

Definition at line 23 of file pointer_predicates.cpp.

◆ pointer_offset()

exprt pointer_offset ( const exprt & pointer )

Definition at line 38 of file pointer_predicates.cpp.

◆ same_object()

exprt same_object	(	const exprt &	p1,
		const exprt &	p2
	)

Definition at line 28 of file pointer_predicates.cpp.

◆ validate_expr()

void validate_expr ( const is_invalid_pointer_exprt & value )