58 if(src.
id()==ID_symbol)
62 else if(src.
id()==ID_dereference)
66 if(op.
id()==ID_address_of)
70 else if(op.
id()==ID_typecast)
89 else if(src.
id()==ID_member)
92 const exprt &op=m.compound();
102 else if(src.
id()==ID_typecast)
139 bitst::const_iterator may_it=
may_bits.find(identifier);
143 bitst::const_iterator must_it=
must_bits.find(identifier);
153 if(rhs.
id()==ID_symbol ||
154 rhs.
id()==ID_dereference)
159 else if(rhs.
id()==ID_typecast)
163 else if(rhs.
id()==ID_if)
168 return merge(v_true, v_false);
175 const exprt &string_expr)
177 if(string_expr.
id()==ID_typecast)
179 else if(string_expr.
id()==ID_address_of)
181 else if(string_expr.
id()==ID_index)
183 else if(string_expr.
id()==ID_string_constant)
196 if(src.
id()==ID_symbol)
198 std::set<exprt> result;
202 else if(src.
id()==ID_dereference)
206 std::set<exprt> pointer_set=
209 std::set<exprt> result;
211 for(
const auto &pointer : pointer_set)
212 if(pointer.
type().
id()==ID_pointer)
219 else if(src.
id()==ID_typecast)
224 return std::set<exprt>();
250 std::set<exprt> lhs_set=cba.
aliases(lhs, from);
254 for(
const auto &lhs_alias : lhs_set)
260 if(lhs.
type().
id()==ID_pointer)
282 switch(instruction.
type)
319 if(
function.
id()==ID_symbol)
323 if(identifier==
"__CPROVER_set_must" ||
324 identifier==
"__CPROVER_clear_must" ||
325 identifier==
"__CPROVER_set_may" ||
326 identifier==
"__CPROVER_clear_may")
328 if(code_function_call.
arguments().size()==2)
336 if(identifier==
"__CPROVER_set_must")
338 else if(identifier==
"__CPROVER_clear_must")
340 else if(identifier==
"__CPROVER_set_may")
342 else if(identifier==
"__CPROVER_clear_may")
349 if(lhs.
type().
id()==ID_pointer)
376 std::set<exprt> lhs_set=cba.
aliases(deref, from);
378 for(
const auto &lhs : lhs_set)
386 else if(identifier==
"memcpy" ||
387 identifier==
"memmove")
389 if(code_function_call.
arguments().size()==3)
402 if(from->function != to->function)
407 code_function_callt::argumentst::const_iterator arg_it=
409 for(
const auto ¶m : code_type.
parameters())
411 const irep_idt &p_identifier=param.get_identifier();
412 if(p_identifier.
empty())
416 if(arg_it==code_function_call.
arguments().end())
422 std::set<exprt> lhs_set=cba.
aliases(p, from);
426 for(
const auto &lhs : lhs_set)
432 if(p.
type().
id()==ID_pointer)
452 if(statement==
"set_may" ||
453 statement==
"set_must" ||
454 statement==
"clear_may" ||
455 statement==
"clear_must")
465 if(statement==
"set_must")
467 else if(statement==
"clear_must")
469 else if(statement==
"set_may")
471 else if(statement==
"clear_may")
478 if(lhs.
type().
id()==ID_pointer)
485 for(bitst::iterator b_it=
may_bits.begin();
495 for(bitst::iterator b_it=
must_bits.begin();
509 std::set<exprt> lhs_set=cba.
aliases(deref, from);
511 for(
const auto &lhs : lhs_set)
528 if(to!=from->get_target())
561 out << bit.first <<
" MAY:";
564 for(
unsigned i=0; b!=0; i++, b>>=1)
577 out << bit.first <<
" MUST:";
580 for(
unsigned i=0; b!=0; i++, b>>=1)
601 bitst::iterator it=
may_bits.begin();
604 while(it!=
may_bits.end() && it->first<bit.first)
606 if(it==
may_bits.end() || bit.first<it->first)
627 while(it!=
must_bits.end() && it->first<bit.first)
632 if(it==
must_bits.end() || bit.first<it->first)
659 for(bitst::iterator a_it=bits.begin();
664 a_it=bits.erase(a_it);
672 if(src.
id()==
"get_must" ||
687 if(src.
id()==
"get_must" || src.
id()==
"get_may")
696 if(pointer.
type().
id()!=ID_pointer)
702 if(src.
id()==
"get_may")
705 if(
get_bit(bit.second, bit_nr))
710 else if(src.
id()==
"get_must")
724 if(src.
id()==
"get_must")
726 else if(src.
id()==
"get_may")
742 *it=
eval(*it, custom_bitvector_analysis);
757 unsigned pass=0, fail=0, unknown=0;
761 if(!f_it->second.body.has_assertion())
765 if(f_it->first==
"__actual_thread_spawn")
769 out <<
"******** Function " << f_it->first <<
'\n';
776 if(i_it->is_assert())
781 if(
operator[](i_it).has_values.is_false())
788 description=i_it->source_location.get_comment();
795 out <<
"<result status=\"";
803 out <<
xml(i_it->source_location);
804 out <<
"<description>" 806 <<
"</description>\n";
807 out <<
"</result>\n\n";
811 out << i_it->source_location;
812 if(!description.
empty())
813 out <<
", " << description;
816 out <<
from_expr(ns, f_it->first, result);
833 out <<
"SUMMARY: " << pass <<
" pass, " << fail <<
" fail, " 834 << unknown <<
" unknown\n";
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
exprt guard
Guard for gotos, assume, assert.
void transform(locationt from, 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...
const irep_idt & get_statement() const
Field-insensitive, location-sensitive bitvector analysis.
const code_declt & to_code_decl(const codet &code)
number_type number(const key_type &a)
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett locationt
std::map< irep_idt, bit_vectort > bitst
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
goto_program_instruction_typet type
What kind of instruction?
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
const componentst & components() const
local_may_alias_factoryt local_may_alias_factory
static irep_idt object2id(const exprt &)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
symbol_tablet symbol_table
Symbol table.
xmlt xml(const source_locationt &location)
static bool get_bit(const bit_vectort src, unsigned bit_nr)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
void make_bottom() final override
no states
Extract member of struct or union.
This class represents an instruction in the GOTO intermediate representation.
void assign_lhs(const exprt &, const vectorst &)
const char * to_string() const
const code_assignt & to_code_assign(const codet &code)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
const irep_idt & id() const
void check(const goto_modelt &, bool xml, std::ostream &)
The boolean constant true.
A declaration of a local variable.
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void set_bit(const exprt &, unsigned bit_nr, modet)
Operator to dereference a pointer.
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool has_get_must_or_may(const exprt &)
const irep_idt & get(const irep_namet &name) const
exprt eval(const exprt &src, custom_bitvector_analysist &) const
vectorst get_rhs(const exprt &) const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
unsigned get_bit_nr(const exprt &)
The boolean constant false.
void instrument(goto_functionst &)
The basic interface of an abstract interpreter.
Base class for all expressions.
const parameterst & parameters() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
exprt eval(const exprt &src, locationt loc)
bool merge(const custom_bitvector_domaint &b, locationt from, locationt to)
A removal of a local variable.
#define Forall_operands(it, expr)
std::set< exprt > aliases(const exprt &, locationt loc)
goto_programt::const_targett locationt
Expression to hold a symbol (variable)
#define forall_goto_functions(it, functions)
unsigned long long bit_vectort
#define forall_goto_program_instructions(it, program)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)