cprover
|
#include <interval_domain.h>
Public Member Functions | |
interval_domaint () | |
void | transform (locationt from, 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 |
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 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'. More... | |
Protected Attributes | |
bool | bottom |
int_mapt | int_map |
float_mapt | float_map |
Additional Inherited Members | |
![]() | |
typedef goto_programt::const_targett | locationt |
Definition at line 24 of file interval_domain.h.
|
protected |
Definition at line 115 of file interval_domain.h.
|
protected |
Definition at line 114 of file interval_domain.h.
|
inline |
Definition at line 31 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 460 of file interval_domain.cpp.
References assume(), irept::id(), is_bottom(), exprt::is_true(), join(), make_top(), and exprt::make_true().
|
protected |
Definition at line 185 of file interval_domain.cpp.
References assume_rec(), havoc_rec(), code_assignt::lhs(), and code_assignt::rhs().
Referenced by transform().
void interval_domaint::assume | ( | const exprt & | cond, |
const namespacet & | ns | ||
) |
Definition at line 327 of file interval_domain.cpp.
References assume_rec(), and simplify_expr().
Referenced by ai_simplify(), and transform().
|
protected |
Definition at line 334 of file interval_domain.cpp.
References forall_operands, irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), and to_not_expr().
Referenced by assign(), assume(), and assume_rec().
Definition at line 213 of file interval_domain.cpp.
References assume_rec(), ieee_floatt::decrement(), float_map, from_expr(), symbol_exprt::get_identifier(), irept::id(), ieee_floatt::increment(), int_map, interval_templatet< T >::is_bottom(), is_float(), is_int(), make_bottom(), interval_templatet< T >::make_ge_than(), interval_templatet< T >::make_le_than(), interval_templatet< T >::meet(), unary_exprt::op(), to_constant_expr(), to_integer(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
|
protected |
|
protected |
|
protected |
Definition at line 191 of file interval_domain.cpp.
References float_map, symbol_exprt::get_identifier(), irept::id(), int_map, is_float(), is_int(), to_if_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
Referenced by assign(), and transform().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 77 of file interval_domain.h.
References bottom, DATA_INVARIANT, float_map, and int_map.
Referenced by ai_simplify().
|
inlinestatic |
Definition at line 102 of file interval_domain.h.
References irept::id().
Referenced by assume_rec(), havoc_rec(), and make_expression().
|
inlinestatic |
Definition at line 97 of file interval_domain.h.
References irept::id().
Referenced by assume_rec(), havoc_rec(), and make_expression().
|
inlinefinaloverridevirtual |
Implements ai_domain_baset.
Definition at line 88 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 127 of file interval_domain.cpp.
References bottom, float_map, int_map, and interval_templatet< T >::join().
Referenced by ai_simplify(), and merge().
|
inlinefinaloverridevirtual |
no states
Implements ai_domain_baset.
Definition at line 57 of file interval_domain.h.
References bottom, float_map, and int_map.
Referenced by assume_rec().
|
inlinefinaloverridevirtual |
a reasonable entry-point state
Implements ai_domain_baset.
Definition at line 72 of file interval_domain.h.
References make_top().
exprt interval_domaint::make_expression | ( | const symbol_exprt & | src | ) | const |
Definition at line 380 of file interval_domain.cpp.
References conjunction(), float_map, from_integer(), symbol_exprt::get_identifier(), int_map, interval_templatet< T >::is_bottom(), is_float(), is_int(), interval_templatet< T >::is_top(), interval_templatet< T >::lower, interval_templatet< T >::lower_set, exprt::type(), interval_templatet< T >::upper, and interval_templatet< T >::upper_set.
Referenced by instrument_intervals().
|
inlinefinaloverridevirtual |
all states – the analysis doesn't use this, and domains may refuse to implement it.
Implements ai_domain_baset.
Definition at line 65 of file interval_domain.h.
References bottom, float_map, and int_map.
Referenced by ai_simplify(), and make_entry().
|
inline |
Definition at line 48 of file interval_domain.h.
References join().
|
overridevirtual |
Reimplemented from ai_domain_baset.
Definition at line 23 of file interval_domain.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 interpretted "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.
References ASSIGN, assign(), ASSUME, assume(), goto_programt::instructiont::code, DEAD, DECL, FUNCTION_CALL, GOTO, goto_programt::instructiont::guard, havoc_rec(), irept::is_not_nil(), code_function_callt::lhs(), code_declt::symbol(), code_deadt::symbol(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_function_call(), and goto_programt::instructiont::type.
|
protected |
Definition at line 112 of file interval_domain.h.
Referenced by is_bottom(), is_top(), join(), make_bottom(), make_top(), and output().
|
protected |
Definition at line 118 of file interval_domain.h.
Referenced by assume_rec(), havoc_rec(), is_bottom(), is_top(), join(), make_bottom(), make_expression(), make_top(), and output().
|
protected |
Definition at line 117 of file interval_domain.h.
Referenced by assume_rec(), havoc_rec(), is_bottom(), is_top(), join(), make_bottom(), make_expression(), make_top(), and output().