cprover
|
#include <custom_bitvector_analysis.h>
Classes | |
struct | vectorst |
Public Types | |
typedef unsigned long long | bit_vectort |
typedef std::map< irep_idt, bit_vectort > | bitst |
![]() | |
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 |
![]() | |
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 | |
![]() | |
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... | |
Definition at line 23 of file custom_bitvector_analysis.h.
typedef unsigned long long custom_bitvector_domaint::bit_vectort |
Definition at line 79 of file custom_bitvector_analysis.h.
typedef std::map<irep_idt, bit_vectort> custom_bitvector_domaint::bitst |
Definition at line 81 of file custom_bitvector_analysis.h.
|
strongprivate |
Enumerator | |
---|---|
SET_MUST | |
CLEAR_MUST | |
SET_MAY | |
CLEAR_MAY |
Definition at line 125 of file custom_bitvector_analysis.h.
|
inline |
Definition at line 115 of file custom_bitvector_analysis.h.
Definition at line 110 of file custom_bitvector_analysis.cpp.
Definition at line 119 of file custom_bitvector_analysis.cpp.
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.
|
inlinestaticprivate |
Definition at line 135 of file custom_bitvector_analysis.h.
|
private |
erase blank bitvectors
Definition at line 674 of file custom_bitvector_analysis.cpp.
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.
|
inlinestaticprivate |
Definition at line 141 of file custom_bitvector_analysis.h.
custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs | ( | const exprt & | rhs | ) | const |
Definition at line 153 of file custom_bitvector_analysis.cpp.
custom_bitvector_domaint::vectorst custom_bitvector_domaint::get_rhs | ( | const irep_idt & | identifier | ) | const |
Definition at line 137 of file custom_bitvector_analysis.cpp.
|
static |
Definition at line 687 of file custom_bitvector_analysis.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 58 of file custom_bitvector_analysis.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 66 of file custom_bitvector_analysis.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 53 of file custom_bitvector_analysis.h.
|
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.
bool custom_bitvector_domaint::merge | ( | const custom_bitvector_domaint & | b, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 609 of file custom_bitvector_analysis.cpp.
|
inlinestatic |
Definition at line 91 of file custom_bitvector_analysis.h.
Definition at line 58 of file custom_bitvector_analysis.cpp.
|
finaloverridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 562 of file custom_bitvector_analysis.cpp.
|
inlinestaticprivate |
Definition at line 130 of file custom_bitvector_analysis.h.
Definition at line 48 of file custom_bitvector_analysis.cpp.
|
private |
Definition at line 23 of file custom_bitvector_analysis.cpp.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 268 of file custom_bitvector_analysis.cpp.
tvt custom_bitvector_domaint::has_values |
Definition at line 113 of file custom_bitvector_analysis.h.
bitst custom_bitvector_domaint::may_bits |
Definition at line 99 of file custom_bitvector_analysis.h.
bitst custom_bitvector_domaint::must_bits |
Definition at line 99 of file custom_bitvector_analysis.h.