Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_INTERVAL_DOMAIN_H
13 #define CPROVER_ANALYSES_INTERVAL_DOMAIN_H
85 "If the domain is bottom the value maps must be empty");
102 return src.
id()==ID_signedbv || src.
id()==ID_unsignedbv;
107 return src.
id()==ID_floatbv;
117 typedef std::map<irep_idt, integer_intervalt>
int_mapt;
131 #endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void assume(const exprt &, const namespacet &)
The type of an expression, extends irept.
static bool is_float(const typet &src)
std::map< irep_idt, integer_intervalt > int_mapt
bool merge(const interval_domaint &b, locationt, locationt)
std::map< irep_idt, ieee_float_intervalt > float_mapt
Base class for all expressions.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void make_entry() final override
Make this domain a reasonable entry-point state.
void assign(const class code_assignt &assignment)
ieee_float_intervalt get_float_rec(const exprt &)
Expression to hold a symbol (variable)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
integer_intervalt get_int_rec(const exprt &)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void assume_rec(const exprt &, bool negation=false)
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
interval_templatet< ieee_floatt > ieee_float_intervalt
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
const irep_idt & id() const
bool is_top() const override final
goto_programt::const_targett locationt
bool is_bottom() const override final
exprt make_expression(const symbol_exprt &) const
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void make_bottom() final override
no states
A codet representing an assignment in the program.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
static bool is_int(const typet &src)
void havoc_rec(const exprt &)