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
 
typedef ai_history_baset::trace_ptrt trace_ptrt
 

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
 
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 void transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)
 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...
 
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' 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 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 110 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 119 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 226 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 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 699 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 153 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 137 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 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 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 91 of file custom_bitvector_analysis.h.

◆ object2id()

irep_idt custom_bitvector_domaint::object2id ( const exprt src)
staticprivate

Definition at line 58 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 130 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 48 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 23 of file custom_bitvector_analysis.cpp.

◆ 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
Deprecated:
SINCE(2019, 08, 01, "use the history signature instead")

Implements ai_domain_baset.

Definition at line 268 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: