cprover
|
#include <interval_domain.h>
Public Member Functions | |
interval_domaint () | |
void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final |
void | output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final |
bool | merge (const interval_domaint &b, locationt from, locationt to) |
void | make_bottom () final |
void | make_top () final |
void | make_entry () final |
exprt | make_expression (const symbol_exprt &) const |
void | assume (const exprt &, const namespacet &) |
bool | is_bottom () const |
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... | |
![]() | |
ai_domain_baset () | |
virtual | ~ai_domain_baset () |
virtual void | transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0 |
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 |
Use the information in the domain to simplify the expression on the LHS of an assignment. 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 &) |
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 106 of file interval_domain.h.
|
protected |
Definition at line 105 of file interval_domain.h.
|
inline |
Definition at line 31 of file interval_domain.h.
References join(), output(), and transform().
|
overridevirtual |
Uses the abstract state to simplify a given expression using context- specific information.
Reimplemented from ai_domain_baset.
Definition at line 454 of file interval_domain.cpp.
References assume(), irept::id(), is_bottom(), exprt::is_true(), join(), make_top(), and exprt::make_true().
Referenced by is_bottom().
|
protected |
Definition at line 179 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 321 of file interval_domain.cpp.
References assume_rec(), and simplify_expr().
Referenced by ai_simplify(), static_analyzert::eval(), make_entry(), and transform().
|
protected |
Definition at line 328 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 207 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(), typecast_exprt::op(), to_constant_expr(), to_integer(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
|
protected |
|
protected |
|
protected |
Definition at line 185 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().
|
inline |
Definition at line 93 of file interval_domain.h.
References ai_simplify(), and bottom.
Referenced by ai_simplify(), and static_analyzert::eval().
|
inlinestatic |
Definition at line 88 of file interval_domain.h.
References irept::id().
Referenced by assume_rec(), havoc_rec(), and make_expression().
|
inlinestatic |
Definition at line 83 of file interval_domain.h.
References irept::id().
Referenced by assume_rec(), havoc_rec(), and make_expression().
|
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 121 of file interval_domain.cpp.
References bottom, float_map, int_map, and interval_templatet< T >::join().
Referenced by ai_simplify(), interval_domaint(), and merge().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 59 of file interval_domain.h.
References bottom, float_map, and int_map.
Referenced by assume_rec().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 74 of file interval_domain.h.
References assume(), make_expression(), and make_top().
exprt interval_domaint::make_expression | ( | const symbol_exprt & | src | ) | const |
Definition at line 374 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(), and make_entry().
|
inlinefinalvirtual |
Implements ai_domain_baset.
Definition at line 67 of file interval_domain.h.
References bottom, float_map, and int_map.
Referenced by ai_simplify(), and make_entry().
|
inline |
Definition at line 50 of file interval_domain.h.
References join().
|
finalvirtual |
Reimplemented from ai_domain_baset.
Definition at line 22 of file interval_domain.cpp.
References bottom, float_map, and int_map.
Referenced by interval_domaint().
|
final |
Definition at line 58 of file interval_domain.cpp.
References ASSIGN, assign(), ASSUME, assume(), DEAD, DECL, FUNCTION_CALL, GOTO, 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(), and to_code_function_call().
Referenced by interval_domaint().
|
protected |
Definition at line 103 of file interval_domain.h.
Referenced by is_bottom(), join(), make_bottom(), make_top(), and output().
|
protected |
Definition at line 109 of file interval_domain.h.
Referenced by assume_rec(), havoc_rec(), join(), make_bottom(), make_expression(), make_top(), and output().
|
protected |
Definition at line 108 of file interval_domain.h.
Referenced by assume_rec(), havoc_rec(), join(), make_bottom(), make_expression(), make_top(), and output().