cprover
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
 

Public Member Functions

void transform (const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt 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, and domains may refuse to implement it. More...
 
void make_entry () final override
 Make this domain a reasonable entry-point state. More...
 
bool is_bottom () const final override
 
bool is_top () const final override
 
bool merge (const custom_bitvector_domaint &b, locationt from, locationt 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 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  modet { modet::SET_MUST, modet::CLEAR_MUST, modet::SET_MAY, modet::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'. 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 79 of file custom_bitvector_analysis.h.

◆ bitst

Definition at line 81 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 125 of file custom_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ custom_bitvector_domaint()

custom_bitvector_domaint::custom_bitvector_domaint ( )
inline

Definition at line 115 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 109 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 118 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 228 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 135 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 659 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 685 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 141 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 152 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 136 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 672 of file custom_bitvector_analysis.cpp.

◆ is_bottom()

bool custom_bitvector_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 58 of file custom_bitvector_analysis.h.

◆ is_top()

bool custom_bitvector_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 66 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_entry()

void custom_bitvector_domaint::make_entry ( )
inlinefinaloverridevirtual

Make this domain a reasonable entry-point state.

Implements ai_domain_baset.

Definition at line 53 of file custom_bitvector_analysis.h.

◆ make_top()

void custom_bitvector_domaint::make_top ( )
inlinefinaloverridevirtual

all states – the analysis doesn't use this, 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,
locationt  from,
locationt  to 
)

Definition at line 594 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 91 of file custom_bitvector_analysis.h.

◆ object2id()

irep_idt custom_bitvector_domaint::object2id ( const exprt src)
staticprivate

Definition at line 57 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 547 of file custom_bitvector_analysis.cpp.

◆ set_bit() [1/3]

void custom_bitvector_domaint::set_bit ( const exprt lhs,
unsigned  bit_nr,
modet  mode 
)
private

Definition at line 47 of file custom_bitvector_analysis.cpp.

◆ set_bit() [2/3]

void custom_bitvector_domaint::set_bit ( const irep_idt identifier,
unsigned  bit_nr,
modet  mode 
)
private

Definition at line 22 of file custom_bitvector_analysis.cpp.

◆ set_bit() [3/3]

static void custom_bitvector_domaint::set_bit ( bit_vectort dest,
unsigned  bit_nr 
)
inlinestaticprivate

Definition at line 130 of file custom_bitvector_analysis.h.

◆ transform()

void custom_bitvector_domaint::transform ( const irep_idt function_from,
locationt  from,
const irep_idt function_to,
locationt  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)

"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())

Implements ai_domain_baset.

Definition at line 270 of file custom_bitvector_analysis.cpp.

Member Data Documentation

◆ has_values

tvt custom_bitvector_domaint::has_values

Definition at line 113 of file custom_bitvector_analysis.h.

◆ may_bits

bitst custom_bitvector_domaint::may_bits

Definition at line 99 of file custom_bitvector_analysis.h.

◆ must_bits

bitst custom_bitvector_domaint::must_bits

Definition at line 99 of file custom_bitvector_analysis.h.


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