34 for(
const auto &interval :
int_map)
36 if(interval.second.is_top())
38 if(interval.second.lower_set)
39 out << interval.second.lower <<
" <= ";
40 out << interval.first;
41 if(interval.second.upper_set)
42 out <<
" <= " << interval.second.upper;
48 if(interval.second.is_top())
50 if(interval.second.lower_set)
51 out << interval.second.lower <<
" <= ";
52 out << interval.first;
53 if(interval.second.upper_set)
54 out <<
" <= " << interval.second.upper;
67 locationt from{trace_from->current_location()};
68 locationt to{trace_to->current_location()};
71 switch(instruction.
type)
91 if(from->get_target() != next)
116 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
132 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
137 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
167 for(int_mapt::iterator it=
int_map.begin();
172 const int_mapt::const_iterator b_it=b.
int_map.find(it->first);
181 it->second.
join(b_it->second);
182 if(it->second!=previous)
189 for(float_mapt::iterator it=
float_map.begin();
192 const float_mapt::const_iterator b_it=b.
float_map.begin();
201 it->second.
join(b_it->second);
202 if(it->second!=previous)
225 else if(lhs.
id()==ID_symbol)
234 else if(lhs.
id()==ID_typecast)
243 if(lhs.
id()==ID_typecast)
246 if(rhs.
id()==ID_typecast)
268 assert(
id==ID_lt ||
id==ID_le);
271 std::cout <<
"assume_rec: "
276 if(lhs.
id()==ID_symbol && rhs.
id()==ID_constant)
301 else if(lhs.
id()==ID_constant && rhs.
id()==ID_symbol)
326 else if(lhs.
id()==ID_symbol && rhs.
id()==ID_symbol)
363 if(cond.
id()==ID_lt || cond.
id()==ID_le ||
364 cond.
id()==ID_gt || cond.
id()==ID_ge ||
365 cond.
id()==ID_equal || cond.
id()==ID_notequal)
371 if(rel.id() == ID_lt)
373 else if(rel.id() == ID_le)
375 else if(rel.id() == ID_gt)
377 else if(rel.id() == ID_ge)
379 else if(rel.id() == ID_equal)
380 assume_rec(rel.op0(), ID_notequal, rel.op1());
381 else if(rel.id() == ID_notequal)
387 else if(cond.
id()==ID_not)
391 else if(cond.
id()==ID_and)
397 else if(cond.
id()==ID_or)
493 if(condition.
id()==ID_and)
505 else if(condition.
id()==ID_symbol)
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
A base class for relations, i.e., binary predicates whose two operands have the same type.
A codet representing an assignment in the program.
codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
The Boolean constant false.
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
goto_program_instruction_typet type
What kind of instruction?
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
void increment(bool distinguish_zero=false)
void decrement(bool distinguish_zero=false)
static bool is_int(const typet &src)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
bool is_bottom() const override final
void make_bottom() final override
no states
void assume_rec(const exprt &, bool negation=false)
void assign(const class code_assignt &assignment)
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
exprt make_expression(const symbol_exprt &) const
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
void havoc_rec(const exprt &)
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.
static bool is_float(const typet &src)
bool is_less_than(const interval_templatet &i)
bool is_less_than_eq(const interval_templatet &i)
void make_le_than(const T &v)
void join(const interval_templatet< T > &i)
void make_ge_than(const T &v)
void make_less_than(interval_templatet &i)
void meet(const interval_templatet< T > &i)
void make_less_than_eq(interval_templatet &i)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The Boolean constant true.
#define forall_operands(it, expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.