56 if(src.
id()==ID_symbol)
60 else if(src.
id()==ID_dereference)
64 if(op.
id()==ID_address_of)
68 else if(op.
id()==ID_typecast)
81 else if(src.
id()==ID_typecast)
118 bitst::const_iterator may_it=
may_bits.find(identifier);
122 bitst::const_iterator must_it=
must_bits.find(identifier);
132 if(rhs.
id()==ID_symbol ||
133 rhs.
id()==ID_dereference)
138 else if(rhs.
id()==ID_typecast)
142 else if(rhs.
id()==ID_if)
147 return merge(v_true, v_false);
154 const exprt &string_expr)
156 if(string_expr.
id()==ID_typecast)
158 else if(string_expr.
id()==ID_address_of)
160 else if(string_expr.
id()==ID_index)
162 else if(string_expr.
id()==ID_string_constant)
168 return bits(
"(unknown)");
175 if(src.
id()==ID_symbol)
177 std::set<exprt> result;
181 else if(src.
id()==ID_dereference)
185 std::set<exprt> pointer_set=
186 local_may_alias_factory(loc).
get(loc, pointer);
188 std::set<exprt> result;
190 for(
const auto &pointer : pointer_set)
199 else if(src.
id()==ID_typecast)
204 return std::set<exprt>();
217 const goto_programt::instructiont &instruction=*from;
219 switch(instruction.type)
226 std::set<exprt> lhs_set=cba.
aliases(code_assign.
lhs(), from);
230 for(
const auto &lhs : lhs_set)
236 if(code_assign.
lhs().
type().
id()==ID_pointer)
274 if(
function.
id()==ID_symbol)
278 if(identifier==
"__CPROVER_set_must" ||
279 identifier==
"__CPROVER_clear_must" ||
280 identifier==
"__CPROVER_set_may" ||
281 identifier==
"__CPROVER_clear_may")
283 if(code_function_call.
arguments().size()==2)
290 if(identifier==
"__CPROVER_set_must")
292 else if(identifier==
"__CPROVER_clear_must")
294 else if(identifier==
"__CPROVER_set_may")
296 else if(identifier==
"__CPROVER_clear_may")
328 std::set<exprt> lhs_set=cba.
aliases(deref, from);
330 for(
const auto &lhs : lhs_set)
348 code_function_callt::argumentst::const_iterator arg_it=
350 for(
const auto ¶m : code_type.
parameters())
352 const irep_idt &p_identifier=param.get_identifier();
353 if(p_identifier.
empty())
357 if(arg_it==code_function_call.
arguments().end())
363 std::set<exprt> lhs_set=cba.
aliases(p, from);
367 for(
const auto &lhs : lhs_set)
373 if(p.
type().
id()==ID_pointer)
391 const irep_idt &statement=instruction.code.get_statement();
393 if(statement==
"set_may" ||
394 statement==
"set_must" ||
395 statement==
"clear_may" ||
396 statement==
"clear_must")
398 assert(instruction.code.operands().size()==2);
405 if(statement==
"set_must")
407 else if(statement==
"clear_must")
409 else if(statement==
"set_may")
411 else if(statement==
"clear_may")
423 for(bitst::iterator b_it=
may_bits.begin();
433 for(bitst::iterator b_it=
must_bits.begin();
447 std::set<exprt> lhs_set=cba.
aliases(deref, from);
449 for(
const auto &lhs : lhs_set)
461 exprt guard=instruction.guard;
463 if(to!=from->get_target())
496 out << bit.first <<
" MAY:";
499 for(
unsigned i=0; b!=0; i++, b>>=1)
502 assert(i<cba.
bits.size());
512 out << bit.first <<
" MUST:";
515 for(
unsigned i=0; b!=0; i++, b>>=1)
518 assert(i<cba.
bits.size());
536 bitst::iterator it=
may_bits.begin();
539 while(it!=
may_bits.end() && it->first<bit.first)
541 if(it==
may_bits.end() || bit.first<it->first)
562 while(it!=
must_bits.end() && it->first<bit.first)
567 if(it==
must_bits.end() || bit.first<it->first)
594 for(bitst::iterator a_it=bits.begin();
599 a_it=bits.erase(a_it);
607 if(src.
id()==
"get_must" ||
622 if(src.
id()==
"get_must" || src.
id()==
"get_may")
634 if(src.
id()==
"get_may")
637 if(
get_bit(bit.second, bit_nr))
642 else if(src.
id()==
"get_must")
656 if(src.
id()==
"get_must")
658 else if(src.
id()==
"get_may")
674 *it=
eval(*it, custom_bitvector_analysis);
690 unsigned pass=0, fail=0, unknown=0;
694 if(!f_it->second.body.has_assertion())
698 if(f_it->first==
"__actual_thread_spawn")
702 out <<
"******** Function " << f_it->first <<
'\n';
709 if(i_it->is_assert())
714 if(
operator[](i_it).has_values.is_false())
720 description=i_it->source_location.get_comment();
727 out <<
"<result status=\"";
735 out <<
xml(i_it->source_location);
736 out <<
"<description>" 738 <<
"</description>\n";
739 out <<
"</result>\n\n";
743 out << i_it->source_location;
744 if(!description.
empty())
745 out <<
", " << description;
747 out <<
from_expr(ns, f_it->first, result);
764 out <<
"SUMMARY: " << pass <<
" pass, " << fail <<
" fail, " 765 << unknown <<
" unknown\n";
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
Field-insensitive, location-sensitive bitvector analysis.
const code_declt & to_code_decl(const codet &code)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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)
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
static irep_idt object2id(const exprt &)
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 assign_lhs(const exprt &, const vectorst &)
const char * to_string() const
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
instructionst::const_iterator const_targett
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
The boolean constant true.
A declaration of a local variable.
void check(const namespacet &, const goto_functionst &, bool xml, std::ostream &)
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
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
#define forall_operands(it, expr)
unsigned get_bit_nr(const exprt &)
The boolean constant false.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
void instrument(goto_functionst &)
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
#define forall_goto_functions(it, functions)
unsigned long long bit_vectort
#define forall_goto_program_instructions(it, program)
const code_function_callt & to_code_function_call(const codet &code)