Loading...

Searching...

No Matches

pointer_predicates.cpp File Reference

Various predicates over pointers in programs. More...

#include "pointer_predicates.h"
#include "arith_tools.h"
#include "c_types.h"
#include "cprover_prefix.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "pointer_offset_size.h"
#include "std_expr.h"
#include "symbol.h"

+ Include dependency graph for pointer_predicates.cpp:

[フレーム]

Go to the source code of this file.

Functions

exprt pointer_object (const exprt &p)

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

exprt object_size (const exprt &pointer)

exprt pointer_offset (const exprt &pointer)

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

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

exprt null_object (const exprt &pointer)

exprt integer_address (const exprt &pointer)

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

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

Detailed Description

Various predicates over pointers in programs.

Definition in file pointer_predicates.cpp.

Function Documentation

◆ 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 & p )

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.