Loading...

Searching...

No Matches

value_set_fit Class Reference

#include <value_set_fi.h>

+ Collaboration diagram for value_set_fit:

[フレーム]

[legend]

Classes

struct entryt

class object_map_dt

Public Types

typedef irep_idt idt

typedef std::optional< mp_integer > offsett

Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.

typedef reference_counting< object_map_dt > object_mapt

typedef std::unordered_set< exprt, irep_hash > expr_sett

typedef std::unordered_set< unsigned int > dynamic_object_id_sett

typedef std::map< idt, entryt > valuest

typedef std::set< idt > flatten_seent

typedef std::unordered_set< idt > gvs_recursion_sett

typedef std::unordered_set< idt > recfind_recursion_sett

typedef std::unordered_set< idt > assign_recursion_sett

Public Member Functions

value_set_fit ()

void set_from (const irep_idt &function, unsigned inx)

void set_to (const irep_idt &function, unsigned inx)

bool offset_is_zero (const offsett &offset) const

exprt to_expr (const object_map_dt::value_type &it) const

void set (object_mapt &dest, const object_map_dt::value_type &it) const

bool insert (object_mapt &dest, const object_map_dt::value_type &it) const

bool insert (object_mapt &dest, const exprt &src) const

bool insert (object_mapt &dest, const exprt &src, const mp_integer &offset_value) const

bool insert (object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const

bool insert (object_mapt &dest, const exprt &expr, const offsett &offset) const

std::vector< exprt > get_value_set (const exprt &expr, const namespacet &ns) const

expr_sett & get (const idt &identifier, const std::string &suffix)

void clear ()

void add_var (const idt &id)

void add_var (const entryt &e)

entryt & get_entry (const idt &id, const std::string &suffix)

entryt & get_entry (const entryt &e)

void add_vars (const std::list< entryt > &vars)

void output (const namespacet &ns, std::ostream &out) const

bool make_union (object_mapt &dest, const object_mapt &src) const

bool make_union (const valuest &new_values)

bool make_union (const value_set_fit &new_values)

void apply_code (const codet &code, const namespacet &ns)

void assign (const exprt &lhs, const exprt &rhs, const namespacet &ns)

void do_function_call (const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)

void do_end_function (const exprt &lhs, const namespacet &ns)

void get_reference_set (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const

Public Attributes

unsigned to_function

unsigned from_function

unsigned to_target_index

unsigned from_target_index

valuest values

bool changed

Static Public Attributes

static object_numberingt object_numbering

static numberingt< irep_idt > function_numbering

Protected Member Functions

void get_reference_set_sharing (const exprt &expr, expr_sett &expr_set, const namespacet &ns) const

void get_value_set_rec (const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const

void get_value_set (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void get_reference_set_sharing (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void get_reference_set_sharing_rec (const exprt &expr, object_mapt &dest, const namespacet &ns) const

void dereference_rec (const exprt &src, exprt &dest) const

void assign_rec (const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)

void flatten (const entryt &e, object_mapt &dest) const

void flatten_rec (const entryt &, object_mapt &, flatten_seent &) const

Detailed Description

Definition at line 29 of file value_set_fi.h.

Member Typedef Documentation

◆ assign_recursion_sett

typedef std::unordered_set<idt> value_set_fit::assign_recursion_sett

Definition at line 198 of file value_set_fi.h.

◆ dynamic_object_id_sett

typedef std::unordered_set<unsigned int> value_set_fit::dynamic_object_id_sett

Definition at line 192 of file value_set_fi.h.

◆ expr_sett

typedef std::unordered_set<exprt, irep_hash> value_set_fit::expr_sett

Definition at line 190 of file value_set_fi.h.

◆ flatten_seent

typedef std::set<idt> value_set_fit::flatten_seent

Definition at line 195 of file value_set_fi.h.

◆ gvs_recursion_sett

typedef std::unordered_set<idt> value_set_fit::gvs_recursion_sett

Definition at line 196 of file value_set_fi.h.

◆ idt

typedef irep_idt value_set_fit::idt

Definition at line 56 of file value_set_fi.h.

◆ object_mapt

typedef reference_counting<object_map_dt> value_set_fit::object_mapt

Definition at line 108 of file value_set_fi.h.

◆ offsett

typedef std::optional<mp_integer> value_set_fit::offsett

Represents the offset into an object: either a unique integer offset, or an unknown value, represented by !offset.

Definition at line 60 of file value_set_fi.h.

◆ recfind_recursion_sett

typedef std::unordered_set<idt> value_set_fit::recfind_recursion_sett

Definition at line 197 of file value_set_fi.h.

◆ valuest

typedef std::map<idt, entryt> value_set_fit::valuest

Definition at line 194 of file value_set_fi.h.

Constructor & Destructor Documentation

◆ value_set_fit()

value_set_fit::value_set_fit ( )

inline

Definition at line 32 of file value_set_fi.h.

Member Function Documentation

◆ add_var() [1/2]

void value_set_fit::add_var ( const entryt & e )

inline

Definition at line 217 of file value_set_fi.h.

◆ add_var() [2/2]

void value_set_fit::add_var ( const idt & id )

inline

Definition at line 212 of file value_set_fi.h.

◆ add_vars()

void value_set_fit::add_vars ( const std::list< entryt > & vars )

inline

Definition at line 237 of file value_set_fi.h.

◆ apply_code()

void value_set_fit::apply_code ( const codet & code,

const namespacet & ns

)

Definition at line 1383 of file value_set_fi.cpp.

◆ assign()

void value_set_fit::assign ( const exprt & lhs,

const exprt & rhs,

const namespacet & ns

)

Definition at line 997 of file value_set_fi.cpp.

◆ assign_rec()

void value_set_fit::assign_rec ( const exprt & lhs,

const object_mapt & values_rhs,

const std::string & suffix,

const namespacet & ns,

assign_recursion_sett & recursion_set

)

protected

Definition at line 1163 of file value_set_fi.cpp.

◆ clear()

void value_set_fit::clear ( )

inline

Definition at line 207 of file value_set_fi.h.

◆ dereference_rec()

void value_set_fit::dereference_rec ( const exprt & src,

exprt & dest

) const

protected

Definition at line 716 of file value_set_fi.cpp.

◆ do_end_function()

void value_set_fit::do_end_function ( const exprt & lhs,

const namespacet & ns

)

Definition at line 1370 of file value_set_fi.cpp.

◆ do_function_call()

void value_set_fit::do_function_call ( const irep_idt & function,

const exprt::operandst & arguments,

const namespacet & ns

)

Definition at line 1321 of file value_set_fi.cpp.

◆ flatten()

void value_set_fit::flatten ( const entryt & e,

object_mapt & dest

) const

protected

Definition at line 133 of file value_set_fi.cpp.

◆ flatten_rec()

void value_set_fit::flatten_rec ( const entryt & e,

object_mapt & dest,

flatten_seent & seen

) const

protected

Definition at line 149 of file value_set_fi.cpp.

◆ get()

expr_sett & value_set_fit::get ( const idt & identifier,

const std::string & suffix

)

◆ get_entry() [1/2]

entryt & value_set_fit::get_entry ( const entryt & e )

inline

Definition at line 227 of file value_set_fi.h.

◆ get_entry() [2/2]

entryt & value_set_fit::get_entry ( const idt & id,

const std::string & suffix

)

inline

Definition at line 222 of file value_set_fi.h.

◆ get_reference_set()

void value_set_fit::get_reference_set ( const exprt & expr,

expr_sett & expr_set,

const namespacet & ns

) const

Definition at line 731 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [1/2]

void value_set_fit::get_reference_set_sharing ( const exprt & expr,

expr_sett & expr_set,

const namespacet & ns

) const

protected

Definition at line 779 of file value_set_fi.cpp.

◆ get_reference_set_sharing() [2/2]

void value_set_fit::get_reference_set_sharing ( const exprt & expr,

object_mapt & dest,

const namespacet & ns

) const

inlineprotected

Definition at line 308 of file value_set_fi.h.

◆ get_reference_set_sharing_rec()

void value_set_fit::get_reference_set_sharing_rec ( const exprt & expr,

object_mapt & dest,

const namespacet & ns

) const

protected

Definition at line 791 of file value_set_fi.cpp.

◆ get_value_set() [1/2]

std::vector< exprt > value_set_fit::get_value_set ( const exprt & expr,

const namespacet & ns

) const

Definition at line 291 of file value_set_fi.cpp.

◆ get_value_set() [2/2]

void value_set_fit::get_value_set ( const exprt & expr,

object_mapt & dest,

const namespacet & ns

) const

protected

Definition at line 352 of file value_set_fi.cpp.

◆ get_value_set_rec()

void value_set_fit::get_value_set_rec ( const exprt & expr,

object_mapt & dest,

bool & includes_nondet_pointer,

const std::string & suffix,

const typet & original_type,

const namespacet & ns,

gvs_recursion_sett & recursion_set

) const

protected

Definition at line 366 of file value_set_fi.cpp.

◆ insert() [1/5]

bool value_set_fit::insert ( object_mapt & dest,

const exprt & expr,

const offsett & offset

) const

inline

Definition at line 168 of file value_set_fi.h.

◆ insert() [2/5]

bool value_set_fit::insert ( object_mapt & dest,

const exprt & src

) const

inline

Definition at line 120 of file value_set_fi.h.

◆ insert() [3/5]

bool value_set_fit::insert ( object_mapt & dest,

const exprt & src,

const mp_integer & offset_value

) const

inline

Definition at line 125 of file value_set_fi.h.

◆ insert() [4/5]

bool value_set_fit::insert ( object_mapt & dest,

const object_map_dt::value_type & it

) const

inline

Definition at line 115 of file value_set_fi.h.

◆ insert() [5/5]

bool value_set_fit::insert ( object_mapt & dest,

object_numberingt::number_type n,

const offsett & offset

) const

inline

Definition at line 133 of file value_set_fi.h.

◆ make_union() [1/3]

bool value_set_fit::make_union ( const value_set_fit & new_values )

inline

Definition at line 261 of file value_set_fi.h.

◆ make_union() [2/3]

bool value_set_fit::make_union ( const valuest & new_values )

Definition at line 239 of file value_set_fi.cpp.

◆ make_union() [3/3]

bool value_set_fit::make_union ( object_mapt & dest,

const object_mapt & src

) const

Definition at line 277 of file value_set_fi.cpp.

◆ offset_is_zero()

bool value_set_fit::offset_is_zero ( const offsett & offset ) const

inline

Definition at line 61 of file value_set_fi.h.

◆ output()

void value_set_fit::output ( const namespacet & ns,

std::ostream & out

) const

Definition at line 36 of file value_set_fi.cpp.

◆ set()

void value_set_fit::set ( object_mapt & dest,

const object_map_dt::value_type & it

) const

inline

Definition at line 110 of file value_set_fi.h.

◆ set_from()

void value_set_fit::set_from ( const irep_idt & function,

unsigned inx

)

inline

Definition at line 44 of file value_set_fi.h.

◆ set_to()

void value_set_fit::set_to ( const irep_idt & function,

unsigned inx

)

inline

Definition at line 50 of file value_set_fi.h.

◆ to_expr()

exprt value_set_fit::to_expr ( const object_map_dt::value_type & it ) const

Definition at line 219 of file value_set_fi.cpp.

Member Data Documentation

◆ changed

bool value_set_fit::changed

Definition at line 252 of file value_set_fi.h.

◆ from_function

unsigned value_set_fit::from_function

Definition at line 39 of file value_set_fi.h.

◆ from_target_index

unsigned value_set_fit::from_target_index

Definition at line 40 of file value_set_fi.h.

◆ function_numbering

numberingt< irep_idt > value_set_fit::function_numbering

static

Definition at line 42 of file value_set_fi.h.

◆ object_numbering

object_numberingt value_set_fit::object_numbering

static

Definition at line 41 of file value_set_fi.h.

◆ to_function

unsigned value_set_fit::to_function

Definition at line 39 of file value_set_fi.h.

◆ to_target_index

unsigned value_set_fit::to_target_index

Definition at line 40 of file value_set_fi.h.

◆ values

valuest value_set_fit::values

Definition at line 250 of file value_set_fi.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_fi.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_fi.cpp