11#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
12#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
27#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
135 const std::vector<symbol_exprt> &lhs,
136 const std::vector<symbol_exprt> &rhs);
169 std::string suffix =
"tmp_cc",
170 bool is_auxiliary =
true);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Stores information about a goto function computed from its CFG, together with a target iterator into ...
goto_programt::targett target
const goto_programt::targett & get_current_target() const
returns the current target instruction
const dirtyt dirty_analysis
void step()
Steps the target iterator forward.
cfg_infot(const namespacet &_ns, goto_functiont &_goto_function)
bool is_not_local_or_dirty_local(irep_idt ident) const
Returns true iff the given ident is either not a goto_function local or is a local that is dirty.
bool is_local(irep_idt ident) const
Returns true iff ident is a local (or parameter) of goto_function.
goto_functiont & goto_function
bool is_maybe_alive(const symbol_exprt &symbol_expr)
Returns true whenever the given symbol_expr might be alive at the current target instruction.
Allows to clean expressions of side effects.
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
cleanert(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
const std::unordered_set< irep_idt > & get_dirty_ids() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
havoc_assigns_targetst(const assignst &mod, const namespacet &ns)
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc a single expression expr
A class that overrides the low-level havocing functions in the base utility class,...
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
havoc_if_validt(const assignst &mod, const namespacet &ns)
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
bool is_local(const irep_idt &identifier) const
Class that provides messages with a built-in verbosity 'level'.
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().
Expression to hold a symbol (variable)
The symbol table base class interface.
The type of an expression, extends irept.
Variables whose address is taken.
Templated functions to cast to specific exprt-derived classes.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Local variables whose address is taken.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void add_pragma_disable_pointer_checks(source_locationt &source_location)
Adds a pragma on a source location disable all pointer checks.
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
void add_pragma_disable_assigns_check(source_locationt &source_location)
Adds a pragma on a source_locationt to disable inclusion checking.
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix="tmp_cc", bool is_auxiliary=true)
Adds a fresh and uniquely named symbol to the symbol table.