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;
68 switch(instruction.
type)
88 if(from->get_target() != next)
113 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
129 DATA_INVARIANT(
false,
"Unclear what is a safe over-approximation of OTHER");
134 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
164 for(int_mapt::iterator it=
int_map.begin();
169 const int_mapt::const_iterator b_it=b.
int_map.find(it->first);
178 it->second.
join(b_it->second);
179 if(it->second!=previous)
186 for(float_mapt::iterator it=
float_map.begin();
189 const float_mapt::const_iterator b_it=b.
float_map.begin();
198 it->second.
join(b_it->second);
199 if(it->second!=previous)
222 else if(lhs.
id()==ID_symbol)
231 else if(lhs.
id()==ID_typecast)
240 if(lhs.
id()==ID_typecast)
243 if(rhs.
id()==ID_typecast)
265 assert(
id==ID_lt ||
id==ID_le);
268 std::cout <<
"assume_rec: "
273 if(lhs.
id()==ID_symbol && rhs.
id()==ID_constant)
298 else if(lhs.
id()==ID_constant && rhs.
id()==ID_symbol)
323 else if(lhs.
id()==ID_symbol && rhs.
id()==ID_symbol)
360 if(cond.
id()==ID_lt || cond.
id()==ID_le ||
361 cond.
id()==ID_gt || cond.
id()==ID_ge ||
362 cond.
id()==ID_equal || cond.
id()==ID_notequal)
368 if(rel.id() == ID_lt)
370 else if(rel.id() == ID_le)
372 else if(rel.id() == ID_gt)
374 else if(rel.id() == ID_ge)
376 else if(rel.id() == ID_equal)
377 assume_rec(rel.op0(), ID_notequal, rel.op1());
378 else if(rel.id() == ID_notequal)
384 else if(cond.
id()==ID_not)
388 else if(cond.
id()==ID_and)
394 else if(cond.
id()==ID_or)
490 if(condition.
id()==ID_and)
502 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...
const code_declt & to_code_decl(const codet &code)
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)
void meet(const interval_templatet< T > &i)
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,...
codet code
Do not read or modify directly – use get_X() instead.
#define forall_operands(it, expr)
void assume_rec(const exprt &, bool negation=false)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
void join(const interval_templatet< T > &i)
void increment(bool distinguish_zero=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
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
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
const code_function_callt & to_code_function_call(const codet &code)
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 code_assignt & to_code_assign(const codet &code)
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.