cprover
Loading...
Searching...
No Matches
pointer_predicates.h File Reference

Various predicates over pointers in programs. More...

#include "std_expr.h"
Include dependency graph for pointer_predicates.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of 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 null_object (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 45 of file pointer_predicates.h.

◆ dead_object()

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

Definition at line 51 of file pointer_predicates.cpp.

◆ deallocated()

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

Definition at line 43 of file pointer_predicates.cpp.

◆ integer_address()

exprt integer_address ( const exprt & pointer)

Definition at line 65 of file pointer_predicates.cpp.

◆ null_object()

exprt null_object ( const exprt & pointer)

Definition at line 59 of file pointer_predicates.cpp.

◆ object_lower_bound()

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

Definition at line 117 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 72 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)
inline

Definition at line 50 of file pointer_predicates.h.