CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp File Reference

CBMC

Loading...

Searching...

No Matches

constant_pointer_abstract_object.cpp File Reference

#include "constant_pointer_abstract_object.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include "abstract_object_statistics.h"
#include <ostream>

+ Include dependency graph for constant_pointer_abstract_object.cpp:

Go to the source code of this file.

Functions

static exprt to_bool_expr (bool v)

exprt struct_member_ptr_comparison_expr (irep_idt const &id, exprt const &lhs, exprt const &rhs)

exprt symbol_ptr_comparison_expr (irep_idt const &id, exprt const &lhs, exprt const &rhs)

Function Documentation

◆ struct_member_ptr_comparison_expr()

exprt struct_member_ptr_comparison_expr ( irep_idt const & id,

exprt const & lhs,

exprt const & rhs

)

Definition at line 323 of file constant_pointer_abstract_object.cpp.

◆ symbol_ptr_comparison_expr()

exprt symbol_ptr_comparison_expr ( irep_idt const & id,

exprt const & lhs,

exprt const & rhs

)

Definition at line 338 of file constant_pointer_abstract_object.cpp.

◆ to_bool_expr()

static exprt to_bool_expr ( bool v )

static

Definition at line 316 of file constant_pointer_abstract_object.cpp.