how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override

void make_bottom () final override

no states

void make_top () final override

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

bool is_bottom () const final override

bool is_top () const final override

bool merge (const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to)

void assign_struct_rec (locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)

void assign_lhs (const exprt &, const vectorst &)

void assign_lhs (const irep_idt &, const vectorst &)

vectorst get_rhs (const exprt &) const

vectorst get_rhs (const irep_idt &) const

custom_bitvector_domaint ()

exprt eval (const exprt &src, custom_bitvector_analysist &) const

- Public Member Functions inherited from ai_domain_baset

virtual ~ai_domain_baset ()

virtual jsont output_json (const ai_baset &ai, const namespacet &ns) const

virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const

virtual void make_entry ()

Make this domain a reasonable entry-point state For most domains top is sufficient.

virtual bool ai_simplify (exprt &condition, const namespacet &) const

also add

virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const

Simplifies the expression but keeps it as an l-value.

virtual exprt to_predicate (void) const

Gives a Boolean condition that is true for all values represented by the domain.

Static Public Member Functions

static vectorst merge (const vectorst &a, const vectorst &b)

static bool has_get_must_or_may (const exprt &)

Public Attributes

bitst may_bits

bitst must_bits

tvt has_values

Private Types

enum class modet { SET_MUST , CLEAR_MUST , SET_MAY , CLEAR_MAY }

Private Member Functions

void set_bit (const exprt &, unsigned bit_nr, modet)

void set_bit (const irep_idt &, unsigned bit_nr, modet)

void erase_blank_vectors (bitst &)

erase blank bitvectors

Static Private Member Functions

static void set_bit (bit_vectort &dest, unsigned bit_nr)

static void clear_bit (bit_vectort &dest, unsigned bit_nr)

static bool get_bit (const bit_vectort src, unsigned bit_nr)

static irep_idt object2id (const exprt &)

Additional Inherited Members

- Protected Member Functions inherited from ai_domain_baset

ai_domain_baset ()

The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface.

ai_domain_baset (const ai_domain_baset &old)

A copy constructor is part of the domain interface.

Detailed Description

Definition at line 23 of file custom_bitvector_analysis.h.

Member Typedef Documentation

◆ bit_vectort

typedef unsigned long long custom_bitvector_domaint::bit_vectort

Definition at line 71 of file custom_bitvector_analysis.h.

◆ bitst

typedef std::map<irep_idt, bit_vectort> custom_bitvector_domaint::bitst

Definition at line 73 of file custom_bitvector_analysis.h.

Member Enumeration Documentation

◆ modet

enum class custom_bitvector_domaint::modet

strongprivate

Enumerator
SET_MUST
CLEAR_MUST
SET_MAY
CLEAR_MAY

Definition at line 117 of file custom_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ custom_bitvector_domaint()

custom_bitvector_domaint::custom_bitvector_domaint ( )

inline

Definition at line 107 of file custom_bitvector_analysis.h.

Member Function Documentation

◆ assign_lhs() [1/2]

void custom_bitvector_domaint::assign_lhs ( const exprt & lhs,

const vectorst & vectors

)

Definition at line 111 of file custom_bitvector_analysis.cpp.

◆ assign_lhs() [2/2]

void custom_bitvector_domaint::assign_lhs ( const irep_idt & identifier,

const vectorst & vectors

)

Definition at line 120 of file custom_bitvector_analysis.cpp.

◆ assign_struct_rec()

void custom_bitvector_domaint::assign_struct_rec ( locationt from,

const exprt & lhs,

const exprt & rhs,

custom_bitvector_analysist & cba,

const namespacet & ns

)

Definition at line 227 of file custom_bitvector_analysis.cpp.

◆ clear_bit()

static void custom_bitvector_domaint::clear_bit ( bit_vectort & dest,

unsigned bit_nr

)

inlinestaticprivate

Definition at line 127 of file custom_bitvector_analysis.h.

◆ erase_blank_vectors()

void custom_bitvector_domaint::erase_blank_vectors ( bitst & bits )

private

erase blank bitvectors

Definition at line 674 of file custom_bitvector_analysis.cpp.

◆ eval()

exprt custom_bitvector_domaint::eval ( const exprt & src,

custom_bitvector_analysist & custom_bitvector_analysis

) const

Definition at line 701 of file custom_bitvector_analysis.cpp.

◆ get_bit()

static bool custom_bitvector_domaint::get_bit ( const bit_vectort src,

unsigned bit_nr

)

inlinestaticprivate

Definition at line 133 of file custom_bitvector_analysis.h.

◆ get_rhs() [1/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const exprt & rhs ) const

Definition at line 154 of file custom_bitvector_analysis.cpp.

◆ get_rhs() [2/2]

custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs ( const irep_idt & identifier ) const

Definition at line 138 of file custom_bitvector_analysis.cpp.

◆ has_get_must_or_may()

bool custom_bitvector_domaint::has_get_must_or_may ( const exprt & src )

static

Definition at line 687 of file custom_bitvector_analysis.cpp.

◆ is_bottom()

bool custom_bitvector_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 53 of file custom_bitvector_analysis.h.

◆ is_top()

bool custom_bitvector_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 61 of file custom_bitvector_analysis.h.

◆ make_bottom()

void custom_bitvector_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 39 of file custom_bitvector_analysis.h.

◆ make_top()

void custom_bitvector_domaint::make_top ( )

inlinefinaloverridevirtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 46 of file custom_bitvector_analysis.h.

◆ merge() [1/2]

bool custom_bitvector_domaint::merge ( const custom_bitvector_domaint & b,

trace_ptrt from,

trace_ptrt to

)

Definition at line 609 of file custom_bitvector_analysis.cpp.

◆ merge() [2/2]

static vectorst custom_bitvector_domaint::merge ( const vectorst & a,

const vectorst & b

)

inlinestatic

Definition at line 83 of file custom_bitvector_analysis.h.

◆ object2id()

irep_idt custom_bitvector_domaint::object2id ( const exprt & src )

staticprivate

Definition at line 59 of file custom_bitvector_analysis.cpp.

◆ output()

void custom_bitvector_domaint::output ( std::ostream & out,

const ai_baset & ai,

const namespacet & ns

) const

finaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 562 of file custom_bitvector_analysis.cpp.

◆ set_bit() [1/3]

static void custom_bitvector_domaint::set_bit ( bit_vectort & dest,

unsigned bit_nr

)

inlinestaticprivate

Definition at line 122 of file custom_bitvector_analysis.h.

◆ set_bit() [2/3]

void custom_bitvector_domaint::set_bit ( const exprt & lhs,

unsigned bit_nr,

modet mode

)

private

Definition at line 49 of file custom_bitvector_analysis.cpp.

◆ set_bit() [3/3]

void custom_bitvector_domaint::set_bit ( const irep_idt & identifier,

unsigned bit_nr,

modet mode

)

private

Definition at line 24 of file custom_bitvector_analysis.cpp.

◆ transform()

void custom_bitvector_domaint::transform ( const irep_idt & function_from,

trace_ptrt from,

const irep_idt & function_to,

trace_ptrt to,

ai_baset & ai,

const namespacet & ns

)

finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implements ai_domain_baset.

Definition at line 271 of file custom_bitvector_analysis.cpp.

Member Data Documentation

◆ has_values

tvt custom_bitvector_domaint::has_values

Definition at line 105 of file custom_bitvector_analysis.h.

◆ may_bits

bitst custom_bitvector_domaint::may_bits

Definition at line 91 of file custom_bitvector_analysis.h.

◆ must_bits

bitst custom_bitvector_domaint::must_bits

Definition at line 91 of file custom_bitvector_analysis.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/custom_bitvector_analysis.h
/home/runner/work/cbmc/cbmc/src/analyses/custom_bitvector_analysis.cpp

custom_bitvector_domaint
Generated by doxygen 1.9.8