95 const exprt &op=m.compound();
198 std::set<exprt> result;
209 std::set<exprt> result;
224 return std::set<exprt>();
250 std::set<exprt>
lhs_set=
cba.aliases(lhs, from);
286 switch(instruction.
type())
295 const auto &decl_symbol = instruction.
decl_symbol();
383 else if(identifier==
"memcpy" ||
384 identifier==
"memmove")
404 code_function_callt::argumentst::const_iterator
arg_it =
446 const auto &code = instruction.
get_other();
447 const irep_idt &statement = code.get_statement();
454 code.operands().size() == 2,
"set/clear_may/must has two operands");
456 unsigned bit_nr =
cba.get_bit_nr(code.op1());
524 if(to!=from->get_target())
536 DATA_INVARIANT(
false,
"Exceptions must be removed before analysis");
539 DATA_INVARIANT(
false,
"SET_RETURN_VALUE must be removed before analysis");
553 DATA_INVARIANT(
false,
"Only complete instructions can be analyzed");
574 out <<
bit.first <<
" MAY:";
577 for(
unsigned i=0;
b!=0;
i++,
b>>=1)
590 out <<
bit.first <<
" MUST:";
593 for(
unsigned i=0;
b!=0;
i++,
b>>=1)
614 bitst::iterator it=
may_bits.begin();
615 for(
const auto &
bit :
b.may_bits)
638 for(
auto &
bit :
b.must_bits)
672 for(bitst::iterator
a_it=bits.begin();
773 if(!
gf_entry.second.body.has_assertion())
777 if(
gf_entry.first ==
"__actual_thread_spawn")
781 out <<
"******** Function " <<
gf_entry.first <<
'\n';
788 if(
i_it->is_assert())
791 i_it->get_condition()))
796 if(
operator[](
i_it).has_values.is_false())
803 description =
i_it->source_location().get_comment();
810 out <<
"<result status=\"";
818 out <<
xml(
i_it->source_location());
819 out <<
"<description>"
821 <<
"</description>\n";
822 out <<
"</result>\n\n";
826 out <<
i_it->source_location();
827 if(!description.
empty())
828 out <<
", " << description;
848 out <<
"SUMMARY: " <<
pass <<
" pass, " <<
fail <<
" fail, "
849 << unknown <<
" unknown\n";
This is the basic interface of the abstract interpreter with default implementations of the core func...
goto_programt::const_targett locationt
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::set< exprt > aliases(const exprt &, locationt loc)
local_may_alias_factoryt local_may_alias_factory
exprt eval(const exprt &src, locationt loc)
void check(const goto_modelt &, bool xml, std::ostream &)
void instrument(goto_functionst &)
unsigned get_bit_nr(const exprt &)
void set_bit(const exprt &, unsigned bit_nr, modet)
bool merge(const custom_bitvector_domaint &b, trace_ptrt from, trace_ptrt to)
std::map< irep_idt, bit_vectort > bitst
static irep_idt object2id(const exprt &)
void assign_struct_rec(locationt from, const exprt &lhs, const exprt &rhs, custom_bitvector_analysist &, const namespacet &)
static bool has_get_must_or_may(const exprt &)
vectorst get_rhs(const exprt &) const
static void clear_bit(bit_vectort &dest, unsigned bit_nr)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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 output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
void assign_lhs(const exprt &, const vectorst &)
void erase_blank_vectors(bitst &)
erase blank bitvectors
static bool get_bit(const bit_vectort src, unsigned bit_nr)
void make_bottom() final override
no states
exprt eval(const exprt &src, custom_bitvector_analysist &) const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const codet & get_other() const
Get the statement for OTHER.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
goto_program_instruction_typet type() const
What kind of instruction?
const irep_idt & id() const
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Extract member of struct or union.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
number_type number(const key_type &a)
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The Boolean constant true.
const char * to_string() const
Field-insensitive, location-sensitive bitvector analysis.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const string_constantt & to_string_constant(const exprt &expr)