#include <interval_domain.h>
|
| 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 |
| 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 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...
|
|
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_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...
|
|
Definition at line 24 of file interval_domain.h.
◆ float_mapt
◆ int_mapt
◆ interval_domaint()
interval_domaint::interval_domaint |
( |
| ) |
|
|
inline |
◆ ai_simplify()
bool interval_domaint::ai_simplify |
( |
exprt & |
condition, |
|
|
const namespacet & |
ns |
|
) |
| const |
|
overridevirtual |
Uses the abstract state to simplify a given expression using context- specific information.
- parameters: The expression to simplify.
- Returns
- A simplified version of the expression.
Reimplemented from ai_domain_baset.
Definition at line 460 of file interval_domain.cpp.
◆ assign()
void interval_domaint::assign |
( |
const class code_assignt & |
assignment | ) |
|
|
protected |
◆ assume()
void interval_domaint::assume |
( |
const exprt & |
cond, |
|
|
const namespacet & |
ns |
|
) |
| |
◆ assume_rec() [1/2]
void interval_domaint::assume_rec |
( |
const exprt & |
cond, |
|
|
bool |
negation = false |
|
) |
| |
|
protected |
◆ assume_rec() [2/2]
◆ get_float_rec()
◆ get_int_rec()
◆ havoc_rec()
void interval_domaint::havoc_rec |
( |
const exprt & |
lhs | ) |
|
|
protected |
◆ is_bottom()
bool interval_domaint::is_bottom |
( |
| ) |
const |
|
inlinefinaloverridevirtual |
◆ is_float()
static bool interval_domaint::is_float |
( |
const typet & |
src | ) |
|
|
inlinestatic |
◆ is_int()
static bool interval_domaint::is_int |
( |
const typet & |
src | ) |
|
|
inlinestatic |
◆ is_top()
bool interval_domaint::is_top |
( |
| ) |
const |
|
inlinefinaloverridevirtual |
◆ join()
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.
- parameters: The interval domain, b, to join to this domain.
- Returns
- True if the join increases the set represented by *this, False if there is no change.
Definition at line 129 of file interval_domain.cpp.
◆ make_bottom()
void interval_domaint::make_bottom |
( |
| ) |
|
|
inlinefinaloverridevirtual |
◆ make_entry()
void interval_domaint::make_entry |
( |
| ) |
|
|
inlinefinaloverridevirtual |
◆ make_expression()
◆ make_top()
void interval_domaint::make_top |
( |
| ) |
|
|
inlinefinaloverridevirtual |
◆ merge()
◆ output()
void interval_domaint::output |
( |
std::ostream & |
out, |
|
|
const ai_baset & |
ai, |
|
|
const namespacet & |
ns |
|
) |
| const |
|
overridevirtual |
◆ transform()
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 59 of file interval_domain.cpp.
◆ bottom
bool interval_domaint::bottom |
|
protected |
◆ float_map
◆ int_map
The documentation for this class was generated from the following files: