CBMC
custom_bitvector_domaint Class Reference

#include <custom_bitvector_analysis.h>

+ Inheritance diagram for custom_bitvector_domaint:
+ Collaboration diagram for custom_bitvector_domaint:

Classes

struct  vectorst
 

Public Types

typedef unsigned long long bit_vectort
 
typedef std::map< irep_idt, bit_vectortbitst
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 

Public Member Functions

void transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
 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) More...
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
 
void make_bottom () final override
 no states More...
 
void make_top () final override
 all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it. More...
 
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. More...
 
virtual bool ai_simplify (exprt &condition, const namespacet &) const
 also add More...
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Simplifies the expression but keeps it as an l-value. More...
 
virtual exprt to_predicate (void) const
 Gives a Boolean condition that is true for all values represented by the domain. More...
 

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 More...
 

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. More...
 
 ai_domain_baset (const ai_domain_baset &old)
 A copy constructor is part of the domain interface. More...
 

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

Definition at line 73 of file custom_bitvector_analysis.h.

Member Enumeration Documentation

◆ modet

enum 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: