32 locationt from{trace_from->current_location()};
33 locationt to{trace_to->current_location()};
36 std::cout <<
"Transform from/to:\n";
37 std::cout << from->location_number <<
" --> " << to->location_number <<
'\n';
41 switch(instruction.
type)
50 ->update_location_context(write_location,
true);
69 ->update_location_context(write_location,
true);
82 if(next != from->get_target())
84 if(to == from->get_target())
147 throw "return instructions should be removed first";
153 throw "threading not supported";
157 throw "exceptions not handled";
168 throw "unrecognised instruction type";
204 std::cout <<
"Merging from/to:\n " << from->location_number <<
" --> "
205 << to->location_number <<
'\n';
220 exprt c = res->to_constant();
224 bool no_simplification =
true;
232 return no_simplification;
236 bool condition_changed = (condition != c);
238 return !condition_changed;
272 if(
function.
id() == ID_symbol)
281 if(to->location_number == next->location_number)
296 for(
const exprt &called_arg : called_arguments)
299 called_arg.type().id() == ID_pointer &&
300 !called_arg.type().subtype().get_bool(ID_C_constant))
308 pointer_value->write(
314 called_arg.type().subtype(), ns,
true,
false),
322 if(symbol.second.is_static_lifetime)
327 symbol.second.type, ns,
true,
false),
341 code_typet::parameterst::const_iterator parameter_it =
342 declaration_parameters.begin();
344 for(
const exprt &called_arg : called_arguments)
346 if(parameter_it == declaration_parameters.end())
349 code_type.
has_ellipsis(),
"Only case for insufficient args");
357 ->update_location_context({from},
true);
362 parameter_it->get_identifier(), called_arg.type());
370 parameter_it == declaration_parameters.end(),
371 "Number of arguments should match parameters");
384 static const std::set<irep_idt> ignored_internal_function = {
393 return ignored_internal_function.find(function_id) !=
394 ignored_internal_function.cend();
412 const std::vector<irep_idt> &modified_symbol_names =
415 std::vector<symbol_exprt> modified_symbols;
416 modified_symbols.reserve(modified_symbol_names.size());
418 modified_symbol_names.begin(),
419 modified_symbol_names.end(),
420 std::back_inserter(modified_symbols),
421 [&ns](
const irep_idt &
id) { return ns.lookup(id).symbol_expr(); });
430 std::vector<symbol_exprt> modified_symbols,
434 for(
const auto &symbol : modified_symbols)
443 variable_sensitivity_domaint::gather_statistics(
const namespacet &ns)
const
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
bool is_bottom() const
Gets whether the domain is bottom.
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
void make_top()
Set the domain to top (i.e. everything)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
bool verify() const
Check the structural invariants are maintained.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
abstract_object_statisticst gather_statistics(const namespacet &ns) const
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
bool is_top() const
Gets whether the domain is top.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
std::set< goto_programt::const_targett > locationst
This is the basic interface of the abstract interpreter with default implementations of the core func...
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
A codet representing an assignment in the program.
codet representation of a function call statement.
exprt::operandst argumentst
std::vector< parametert > parameterst
bool has_ellipsis() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
This class represents an instruction in the GOTO intermediate representation.
codet code
Do not read or modify directly – use get_X() instead.
goto_program_instruction_typet type
What kind of instruction?
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const irep_idt & id() const
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().
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
typet type
Type of symbol.
bool ai_simplify(exprt &condition, const namespacet &ns) const override
Use the information in the domain to simplify the expression with respect to the current location.
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void make_top() override
Sets the domain to top (all states).
void apply_domain(std::vector< symbol_exprt > modified_symbols, const variable_sensitivity_domaint &target, const namespacet &ns)
Given a domain and some symbols, apply those symbols values to the current domain.
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) override
Compute the abstract transformer for a single instruction.
abstract_environmentt abstract_state
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
bool is_bottom() const override
Find out if the domain is currently unreachable.
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
void transform_function_call(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.
flow_sensitivityt flow_sensitivity
bool is_top() const override
Is the domain completely top at this state.
bool ignore_function_call_transform(const irep_idt &function_id) const
Used to specify which CPROVER internal functions should be skipped over when doing function call tran...
void make_entry() override
Set up a reasonable entry-point state.
#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)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
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.
There are different ways of handling arrays, structures, unions and pointers.