Go to the documentation of this file.
59 if(src.
id()==ID_symbol)
63 else if(src.
id()==ID_dereference)
67 if(op.
id()==ID_address_of)
71 else if(op.
id()==ID_typecast)
90 else if(src.
id()==ID_member)
93 const exprt &op=m.compound();
103 else if(src.
id()==ID_typecast)
140 bitst::const_iterator may_it=
may_bits.find(identifier);
144 bitst::const_iterator must_it=
must_bits.find(identifier);
154 if(rhs.
id()==ID_symbol ||
155 rhs.
id()==ID_dereference)
160 else if(rhs.
id()==ID_typecast)
164 else if(rhs.
id()==ID_if)
169 return merge(v_true, v_false);
176 const exprt &string_expr)
178 if(string_expr.
id()==ID_typecast)
180 else if(string_expr.
id()==ID_address_of)
182 else if(string_expr.
id()==ID_index)
184 else if(string_expr.
id()==ID_string_constant)
197 if(src.
id()==ID_symbol)
199 std::set<exprt> result;
203 else if(src.
id()==ID_dereference)
207 const std::set<exprt> alias_set =
210 std::set<exprt> result;
212 for(
const auto &alias : alias_set)
213 if(alias.type().id() == ID_pointer)
220 else if(src.
id()==ID_typecast)
225 return std::set<exprt>();
251 std::set<exprt> lhs_set=cba.
aliases(lhs, from);
255 for(
const auto &lhs_alias : lhs_set)
261 if(lhs.
type().
id()==ID_pointer)
280 static_cast<custom_bitvector_analysist &>(ai);
284 switch(instruction.
type)
321 if(
function.
id()==ID_symbol)
331 if(code_function_call.
arguments().size()==2)
352 if(lhs.
type().
id()==ID_pointer)
379 std::set<exprt> lhs_set=cba.
aliases(deref, from);
381 for(
const auto &l : lhs_set)
389 else if(identifier==
"memcpy" ||
390 identifier==
"memmove")
392 if(code_function_call.
arguments().size()==3)
405 if(function_from != function_to)
410 code_function_callt::argumentst::const_iterator arg_it=
412 for(
const auto ¶m : code_type.
parameters())
414 const irep_idt &p_identifier=param.get_identifier();
415 if(p_identifier.
empty())
419 if(arg_it==code_function_call.
arguments().end())
425 std::set<exprt> lhs_set=cba.
aliases(p, from);
429 for(
const auto &lhs : lhs_set)
435 if(p.
type().
id()==ID_pointer)
454 if(statement==
"set_may" ||
455 statement==
"set_must" ||
456 statement==
"clear_may" ||
457 statement==
"clear_must")
467 if(statement==
"set_must")
469 else if(statement==
"clear_must")
471 else if(statement==
"set_may")
473 else if(statement==
"clear_may")
480 if(lhs.
type().
id()==ID_pointer)
487 for(bitst::iterator b_it=
may_bits.begin();
497 for(bitst::iterator b_it=
must_bits.begin();
511 std::set<exprt> lhs_set=cba.
aliases(deref, from);
513 for(
const auto &l : lhs_set)
530 if(to!=from->get_target())
559 static_cast<const custom_bitvector_analysist &>(ai);
563 out << bit.first <<
" MAY:";
566 for(
unsigned i=0; b!=0; i++, b>>=1)
579 out << bit.first <<
" MUST:";
582 for(
unsigned i=0; b!=0; i++, b>>=1)
603 bitst::iterator it=
may_bits.begin();
606 while(it!=
may_bits.end() && it->first<bit.first)
608 if(it==
may_bits.end() || bit.first<it->first)
629 while(it!=
must_bits.end() && it->first<bit.first)
634 if(it==
must_bits.end() || bit.first<it->first)
661 for(bitst::iterator a_it=bits.begin();
666 a_it=bits.erase(a_it);
674 if(src.
id()==
"get_must" ||
689 if(src.
id()==
"get_must" || src.
id()==
"get_may")
698 if(pointer.
type().
id()!=ID_pointer)
704 if(src.
id()==
"get_may")
707 if(
get_bit(bit.second, bit_nr))
712 else if(src.
id()==
"get_must")
726 if(src.
id()==
"get_must")
728 else if(src.
id()==
"get_may")
744 *it=
eval(*it, custom_bitvector_analysis);
759 unsigned pass=0, fail=0, unknown=0;
763 if(!f_it->second.body.has_assertion())
767 if(f_it->first==
"__actual_thread_spawn")
771 out <<
"******** Function " << f_it->first <<
'\n';
778 if(i_it->is_assert())
783 if(
operator[](i_it).has_values.is_false())
790 description=i_it->source_location.get_comment();
797 out <<
"<result status=\"";
805 out <<
xml(i_it->source_location);
806 out <<
"<description>"
808 <<
"</description>\n";
809 out <<
"</result>\n\n";
813 out << i_it->source_location;
814 if(!description.
empty())
815 out <<
", " << description;
818 out <<
from_expr(ns, f_it->first, result);
835 out <<
"SUMMARY: " << pass <<
" pass, " << fail <<
" fail, "
836 << unknown <<
" unknown\n";
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void assign_lhs(const exprt &, const vectorst &)
static irep_idt object2id(const exprt &)
#define Forall_operands(it, expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_declt & to_code_decl(const codet &code)
goto_programt::const_targett locationt
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
void erase_blank_vectors(bitst &)
erase blank bitvectors
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
goto_program_instruction_typet type
What kind of instruction?
vectorst get_rhs(const exprt &) const
xmlt xml(const source_locationt &location)
A codet representing the declaration of a local variable.
Base class for all expressions.
exprt eval(const exprt &src, locationt loc)
void set_bit(const exprt &, unsigned bit_nr, modet)
void instrument(goto_functionst &)
std::set< exprt > aliases(const exprt &, locationt loc)
bool is_true() const
Return whether the expression is a constant representing true.
Expression to hold a symbol (variable)
exprt simplify_expr(const exprt &src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
bool is_false() const
Return whether the expression is a constant representing false.
number_type number(const key_type &a)
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
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.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
const code_deadt & to_code_dead(const codet &code)
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
const char * to_string() const
The Boolean constant false.
A codet representing the removal of a local variable going out of scope.
const parameterst & parameters() const
Extract member of struct or union.
Deprecated expression utility functions.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static bool has_get_must_or_may(const exprt &)
goto_programt::const_targett locationt
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
unsigned long long bit_vectort
Structure type, corresponds to C style structs.
goto_functionst goto_functions
GOTO functions.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
local_may_alias_factoryt local_may_alias_factory
exprt guard
Guard for gotos, assume, assert.
The basic interface of an abstract interpreter.
exprt eval(const exprt &src, custom_bitvector_analysist &) const
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt 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 check(const goto_modelt &, bool xml, std::ostream &)
#define forall_goto_functions(it, functions)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
A codet representing an assignment in the program.
The Boolean constant true.
const irep_idt & get_statement() const
This class represents an instruction in the GOTO intermediate representation.
std::map< irep_idt, bit_vectort > bitst
const irep_idt & get_value() const
symbol_tablet symbol_table
Symbol table.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
#define forall_goto_program_instructions(it, program)
unsigned get_bit_nr(const exprt &)
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
static bool get_bit(const bit_vectort src, unsigned bit_nr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void make_bottom() final override
no states