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)
335 if(identifier==
"__CPROVER_set_must")
337 else if(identifier==
"__CPROVER_clear_must")
339 else if(identifier==
"__CPROVER_set_may")
341 else if(identifier==
"__CPROVER_clear_may")
348 if(lhs.
type().
id()==ID_pointer)
375 std::set<exprt> lhs_set=cba.
aliases(deref, from);
377 for(
const auto &lhs : lhs_set)
385 else if(identifier==
"memcpy" ||
386 identifier==
"memmove")
388 if(code_function_call.
arguments().size()==3)
401 if(from->function != to->function)
406 code_function_callt::argumentst::const_iterator arg_it=
408 for(
const auto ¶m : code_type.
parameters())
410 const irep_idt &p_identifier=param.get_identifier();
411 if(p_identifier.
empty())
415 if(arg_it==code_function_call.
arguments().end())
421 std::set<exprt> lhs_set=cba.
aliases(p, from);
425 for(
const auto &lhs : lhs_set)
431 if(p.
type().
id()==ID_pointer)
451 if(statement==
"set_may" ||
452 statement==
"set_must" ||
453 statement==
"clear_may" ||
454 statement==
"clear_must")
463 if(statement==
"set_must")
465 else if(statement==
"clear_must")
467 else if(statement==
"set_may")
469 else if(statement==
"clear_may")
476 if(lhs.
type().
id()==ID_pointer)
483 for(bitst::iterator b_it=
may_bits.begin();
493 for(bitst::iterator b_it=
must_bits.begin();
507 std::set<exprt> lhs_set=cba.
aliases(deref, from);
509 for(
const auto &lhs : lhs_set)
526 if(to!=from->get_target())
559 out << bit.first <<
" MAY:";
562 for(
unsigned i=0; b!=0; i++, b>>=1)
575 out << bit.first <<
" MUST:";
578 for(
unsigned i=0; b!=0; i++, b>>=1)
599 bitst::iterator it=
may_bits.begin();
602 while(it!=
may_bits.end() && it->first<bit.first)
604 if(it==
may_bits.end() || bit.first<it->first)
625 while(it!=
must_bits.end() && it->first<bit.first)
630 if(it==
must_bits.end() || bit.first<it->first)
657 for(bitst::iterator a_it=bits.begin();
662 a_it=bits.erase(a_it);
670 if(src.
id()==
"get_must" ||
685 if(src.
id()==
"get_must" || src.
id()==
"get_may")
694 if(pointer.
type().
id()!=ID_pointer)
700 if(src.
id()==
"get_may")
703 if(
get_bit(bit.second, bit_nr))
708 else if(src.
id()==
"get_must")
722 if(src.
id()==
"get_must")
724 else if(src.
id()==
"get_may")
740 *it=
eval(*it, custom_bitvector_analysis);
755 unsigned pass=0, fail=0, unknown=0;
759 if(!f_it->second.body.has_assertion())
763 if(f_it->first==
"__actual_thread_spawn")
767 out <<
"******** Function " << f_it->first <<
'\n';
774 if(i_it->is_assert())
779 if(
operator[](i_it).has_values.is_false())
786 description=i_it->source_location.get_comment();
793 out <<
"<result status=\"";
801 out <<
xml(i_it->source_location);
802 out <<
"<description>" 804 <<
"</description>\n";
805 out <<
"</result>\n\n";
809 out << i_it->source_location;
810 if(!description.
empty())
811 out <<
", " << description;
814 out <<
from_expr(ns, f_it->first, result);
831 out <<
"SUMMARY: " << pass <<
" pass, " << fail <<
" fail, " 832 << 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
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
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.
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 &)
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)