cprover
|
#include <constant_propagator.h>
Classes | |
struct | valuest |
Public Member Functions | |
virtual void | transform (const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai_base, 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... | |
virtual void | output (std::ostream &out, const ai_baset &ai_base, const namespacet &ns) const override |
bool | merge (const constant_propagator_domaint &other, locationt from, locationt to) |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const final override |
Simplify the condition given context-sensitive knowledge from the abstract state. More... | |
virtual void | make_bottom () final override |
no states More... | |
virtual void | make_top () final override |
all states – the analysis doesn't use this, and domains may refuse to implement it. More... | |
virtual void | make_entry () final override |
Make this domain a reasonable entry-point state. More... | |
virtual bool | is_bottom () const final override |
virtual bool | is_top () const final override |
bool | partial_evaluate (exprt &expr, const namespacet &ns) const |
Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it. More... | |
![]() | |
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_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... | |
Public Attributes | |
valuest | values |
Protected Member Functions | |
void | assign_rec (valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns, const constant_propagator_ait *cp) |
bool | two_way_propagate_rec (const exprt &expr, const namespacet &ns, const constant_propagator_ait *cp) |
handles equalities and conjunctions containing equalities More... | |
bool | partial_evaluate_with_all_rounding_modes (exprt &expr, const namespacet &ns) const |
Attempt to evaluate an expression in all rounding modes. More... | |
bool | replace_constants_and_simplify (exprt &expr, const namespacet &ns) const |
![]() | |
ai_domain_baset () | |
The constructor is expected to produce 'false' or 'bottom'. More... | |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 33 of file constant_propagator.h.
|
finaloverridevirtual |
Simplify the condition given context-sensitive knowledge from the abstract state.
Reimplemented from ai_domain_baset.
Definition at line 288 of file constant_propagator.cpp.
|
protected |
Definition at line 31 of file constant_propagator.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 73 of file constant_propagator.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 78 of file constant_propagator.h.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 68 of file constant_propagator.h.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 63 of file constant_propagator.h.
bool constant_propagator_domaint::merge | ( | const constant_propagator_domaint & | other, |
locationt | from, | ||
locationt | to | ||
) |
Definition at line 524 of file constant_propagator.cpp.
|
overridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 405 of file constant_propagator.cpp.
bool constant_propagator_domaint::partial_evaluate | ( | exprt & | expr, |
const namespacet & | ns | ||
) | const |
Attempt to evaluate expression using domain knowledge This function changes the expression that is passed into it.
expr | The expression to evaluate |
ns | The namespace for symbols in the expression |
Definition at line 537 of file constant_propagator.cpp.
|
protected |
Attempt to evaluate an expression in all rounding modes.
If the result is the same for all rounding modes, change expr to that result and return false. Otherwise, return true.
Definition at line 555 of file constant_propagator.cpp.
|
protected |
Definition at line 591 of file constant_propagator.cpp.
|
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 60 of file constant_propagator.cpp.
|
protected |
handles equalities and conjunctions containing equalities
Definition at line 233 of file constant_propagator.cpp.
valuest constant_propagator_domaint::values |
Definition at line 138 of file constant_propagator.h.