Go to the documentation of this file.
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void make_ge_than(const T &v)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
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...
void assume(const exprt &, const namespacet &)
void decrement(bool distinguish_zero=false)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
goto_program_instruction_typet type
What kind of instruction?
static bool is_float(const typet &src)
void make_less_than_eq(interval_templatet &i)
bool is_less_than(const interval_templatet &i)
Base class for all expressions.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void assign(const class code_assignt &assignment)
bool is_true() const
Return whether the expression is a constant representing true.
Expression to hold a symbol (variable)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
void meet(const interval_templatet< T > &i)
ai_history_baset::trace_ptrt trace_ptrt
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
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...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
#define forall_operands(it, expr)
void assume_rec(const exprt &, bool negation=false)
const irep_idt & get_identifier() const
void join(const interval_templatet< T > &i)
void increment(bool distinguish_zero=false)
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 code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
exprt simplify_expr(exprt src, const namespacet &ns)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool is_less_than_eq(const interval_templatet &i)
const irep_idt & id() const
std::vector< exprt > operandst
The Boolean constant false.
goto_programt::const_targett locationt
void make_less_than(interval_templatet &i)
bool is_bottom() const override final
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
exprt make_expression(const symbol_exprt &) const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
A base class for relations, i.e., binary predicates whose two operands have the same type.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void make_bottom() final override
no states
void make_le_than(const T &v)
A codet representing an assignment in the program.
The Boolean constant true.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
static bool is_int(const typet &src)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void havoc_rec(const exprt &)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.