41 const goto_functionst::function_mapt::const_iterator,
68 const std::unordered_set<symbol_exprt, irep_hash> &)
const;
110 const std::string &suffix)
const
113 state_prefix + std::to_string(loc->location_number) + suffix;
128 std::vector<symbol_exprt> symbols;
165 const exprt &what)
const
182 std::to_string(loc->location_number) +
"-" +
186 return std::move(symbol);
201 for(
auto &op :
tmp.operands())
211 const std::unordered_set<symbol_exprt, irep_hash> &
bound_symbols)
const
325 else if(what.
operands().size() == 3)
337 DATA_INVARIANT(
false,
"is_sentinel_dll expressions have 2 or 3 operands");
375 for(
auto &op :
tmp.operands())
408 std::move(condition)),
484 "address of side effect " +
614 incoming[it->get_target()].push_back(it);
619 auto next = std::next(it);
620 if(it->is_goto() && it->condition().is_true())
653 auto identifier = function.get_identifier();
659 if(identifier ==
"malloc")
675 if(identifier ==
"posix_memalign")
692 if(identifier ==
"realloc")
712 if(identifier ==
"free")
726 auto f =
goto_model.goto_functions.function_map.find(identifier);
727 if(f ==
goto_model.goto_functions.function_map.end())
731 if(!f->second.body_available())
734 if(loc->call_lhs().is_not_nil())
737 loc->call_lhs().type(), loc->source_location());
748 std::cout <<
"**** WARNING: no body for function " << identifier <<
'\n';
764 const auto &arguments = loc->call_arguments();
767 for(std::size_t i = 0; i < type.parameters().size(); i++)
770 f->second.parameter_identifiers[i], type.parameters()[i].type()));
776 if(arguments.size() > type.parameters().size())
781 for(std::size_t i = type.parameters().size(); i < arguments.size(); i++)
783 auto index = i - type.parameters().size();
785 std::to_string(loc->location_number) +
786 "::" + std::to_string(index);
800 "va_arg_array::" +
state_prefix + std::to_string(loc->location_number);
803 for(std::size_t i = 0; i <
va_count; i++)
830 state_prefix + std::to_string(loc->location_number) +
".";
844 auto exit_loc = std::prev(f->second.body.instructions.end());
854 if(loc->call_lhs().is_not_nil())
856 auto rhs =
symbol_exprt(
"return_value", loc->call_lhs().type());
880 const auto &function = loc->call_function();
885 "can't do function pointers", loc->source_location());
894 false,
"got function that's neither a symbol nor a function pointer");
899 goto_functionst::function_mapt::const_iterator
f_entry,
902 const auto &goto_function =
f_entry->second;
904 if(goto_function.body.instructions.empty())
932 const std::string &state_prefix,
933 const std::vector<irep_idt> &call_stack,
934 const std::string &annotation,
936 const exprt &return_lhs,
975 auto &lhs = loc->assign_lhs();
976 auto &rhs = loc->assign_rhs();
978 DATA_INVARIANT(lhs.type() == rhs.type(),
"assignment type consistency");
1000 else if(loc->is_assume())
1011 else if(loc->is_goto())
1014 const auto &condition = loc->condition();
1016 if(condition.is_true())
1036 else if(loc->is_assert())
1045 loc->is_skip() || loc->is_assert() || loc->is_location() ||
1046 loc->is_end_function())
1051 else if(loc->is_atomic_begin() || loc->is_atomic_end())
1056 else if(loc->is_other())
1058 auto &code = loc->code();
1059 auto &statement = code.get_statement();
1063 code.operands().size() == 2,
"array_set has two operands");
1073 else if(loc->is_decl())
1081 else if(loc->is_dead())
1090 else if(loc->is_function_call())
1094 else if(loc->is_set_return_value())
1096 const auto &rhs = loc->return_value();
1110 std::cout <<
"X: " << loc->type() <<
'\n';
1141 "The given function was not found",
"contract");
1145 "The given function has no contract",
"contract");
1160 for(
auto &f : sorted)
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
std::vector< symbol_exprt > variablest
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Operator to return the address of an array element relative to a base address.
virtual void annotation(const std::string &)
void set_source_location(source_locationt __source_location)
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
Operator to return the address of a field relative to a base address.
Application of (mathematical) function.
function_mapt function_map
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::string & id_string() const
const irep_idt & id() const
A (mathematical) lambda expression.
Extract member of struct or union.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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().
Operator to return the address of an object.
A side_effect_exprt that returns a non-deterministically chosen value.
state_encodingt(const goto_modelt &__goto_model)
exprt evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const
void setup_incoming(const goto_functiont &)
symbol_exprt in_state_expr(loct) const
void function_call(goto_programt::const_targett, encoding_targett &)
const goto_modelt & goto_model
exprt address_rec(loct, const exprt &, exprt) const
goto_programt::const_targett loct
void encode(const goto_functiont &, const irep_idt function_identifier, const std::string &state_prefix, const std::vector< irep_idt > &call_stack, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)
symbol_exprt out_state_expr(loct) const
static symbol_exprt va_args(irep_idt function)
exprt assignment_constraint_rec(loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) const
std::map< loct, std::vector< loct >, goto_programt::target_less_than > incomingt
exprt replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const
void function_call_symbol(goto_programt::const_targett, encoding_targett &)
exprt evaluate_expr(loct, const exprt &, const exprt &) const
irep_idt function_identifier
symbol_exprt state_expr_with_suffix(loct, const std::string &suffix) const
std::vector< irep_idt > call_stack
exprt assignment_constraint(loct, exprt lhs, exprt rhs) const
std::vector< symbol_exprt > incoming_symbols(loct) const
void operator()(const goto_functionst::function_mapt::const_iterator, encoding_targett &)
static exprt state_lambda_expr(exprt)
exprt forall_states_expr(loct, exprt) const
Expression to hold a symbol (variable)
irep_idt name
The unique identifier.
An expression with three operands.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
void equality_propagation(std::vector< exprt > &constraints)
#define forall_goto_program_instructions(it, program)
static symbol_exprt state_expr()
static exprt simplifying_not(exprt src)
static mathematical_function_typet state_predicate_type()
std::optional< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &ns)
Instrument Given Invariants.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
API to expression classes for Pointers.
const live_object_exprt & to_live_object_expr(const exprt &expr)
Cast an exprt to a live_object_exprt.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const cstrlen_exprt & to_cstrlen_expr(const exprt &expr)
Cast an exprt to a cstrlen_exprt.
const writeable_object_exprt & to_writeable_object_expr(const exprt &expr)
Cast an exprt to a writeable_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
solver_resultt state_encoding_solver(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &solver_options)
void state_encoding(const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, encoding_targett &dest)
void variable_encoding(const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, std::ostream &out)
std::set< irep_idt > no_body_warnings
static exprt simplifying_not(exprt src)
side_effect_exprt & to_side_effect_expr(exprt &expr)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_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_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
A total order over targett and const_targett.