cprover
|
#include <interval_domain.h>
Public Member Functions | |
interval_domaint () | |
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 override |
bool | merge (const interval_domaint &b, locationt, locationt) |
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 override final |
bool | is_top () const override final |
exprt | make_expression (const symbol_exprt &) const |
void | assume (const exprt &, const namespacet &) |
virtual bool | ai_simplify (exprt &condition, const namespacet &ns) const override |
Uses the abstract state to simplify a given expression using context- specific information. More... | |
![]() | |
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_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 bool | is_int (const typet &src) |
static bool | is_float (const typet &src) |
Protected Types | |
typedef std::map< irep_idt, integer_intervalt > | int_mapt |
typedef std::map< irep_idt, ieee_float_intervalt > | float_mapt |
Protected Member Functions | |
bool | join (const interval_domaint &b) |
Sets *this to the mathematical join between the two domains. More... | |
void | havoc_rec (const exprt &) |
void | assume_rec (const exprt &, bool negation=false) |
void | assume_rec (const exprt &lhs, irep_idt id, const exprt &rhs) |
void | assign (const class code_assignt &assignment) |
integer_intervalt | get_int_rec (const exprt &) |
ieee_float_intervalt | get_float_rec (const exprt &) |
![]() | |
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... | |
Protected Attributes | |
bool | bottom |
int_mapt | int_map |
float_mapt | float_map |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
typedef ai_history_baset::trace_ptrt | trace_ptrt |
Definition at line 23 of file interval_domain.h.
|
protected |
Definition at line 118 of file interval_domain.h.
|
protected |
Definition at line 117 of file interval_domain.h.
|
inline |
Definition at line 30 of file interval_domain.h.
|
overridevirtual |
Uses the abstract state to simplify a given expression using context- specific information.
Reimplemented from ai_domain_baset.
Definition at line 482 of file interval_domain.cpp.
|
protected |
Definition at line 209 of file interval_domain.cpp.
void interval_domaint::assume | ( | const exprt & | cond, |
const namespacet & | ns | ||
) |
Definition at line 349 of file interval_domain.cpp.
|
protected |
Definition at line 356 of file interval_domain.cpp.
Definition at line 237 of file interval_domain.cpp.
|
protected |
|
protected |
|
protected |
Definition at line 215 of file interval_domain.cpp.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 80 of file interval_domain.h.
|
inlinestatic |
Definition at line 105 of file interval_domain.h.
|
inlinestatic |
Definition at line 100 of file interval_domain.h.
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 91 of file interval_domain.h.
|
protected |
Sets *this to the mathematical join between the two domains.
This can be thought of as an abstract version of union; *this is increased so that it contains all of the values that are represented by b as well as its original intervals. The result is an overapproximation, for example: "[0,1]".join("[3,4]") --> "[0,4]" includes 2 which isn't in [0,1] or [3,4].
Join is used in several places, the most significant being merge, which uses it to bring together two different paths of analysis.
Definition at line 151 of file interval_domain.cpp.
|
inlinefinaloverridevirtual |
|
inlinefinaloverridevirtual |
Make this domain a reasonable entry-point state.
Implements ai_domain_baset.
Definition at line 75 of file interval_domain.h.
exprt interval_domaint::make_expression | ( | const symbol_exprt & | src | ) | const |
Definition at line 402 of file interval_domain.cpp.
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 68 of file interval_domain.h.
|
inline |
Definition at line 51 of file interval_domain.h.
|
overridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 23 of file interval_domain.cpp.
|
finaloverridevirtual |
Implements ai_domain_baset.
Definition at line 59 of file interval_domain.cpp.
|
protected |
Definition at line 115 of file interval_domain.h.
|
protected |
Definition at line 121 of file interval_domain.h.
|
protected |
Definition at line 120 of file interval_domain.h.