29 const std::function<
void()> &havoc_code_impl)
70 if(expr.
id() == ID_pointer_object)
82 location.
add_pragma(
"disable:pointer-primitive-check");
83 location.
add_pragma(
"disable:pointer-overflow-check");
84 location.
add_pragma(
"disable:signed-overflow-check");
85 location.
add_pragma(
"disable:unsigned-overflow-check");
86 location.
add_pragma(
"disable:conversion-check");
126 if(expr.
id() == ID_dereference)
127 validity_checks.push_back(
130 for(
const auto &op : expr.
operands())
137 const std::vector<symbol_exprt> &lhs,
138 const std::vector<symbol_exprt> &rhs)
155 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
158 equality_conjunctions[i] =
159 and_exprt(equality_conjunctions[i - 1], component_i_equality);
169 lexicographic_individual_comparisons[0] =
171 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
174 lexicographic_individual_comparisons[i] =
175 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
177 return disjunction(lexicographic_individual_comparisons);
187 std::advance(target, offset);
209 instruction.is_goto() &&
211 instruction.turn_into_skip();
227 "Instruction list vs CFG size mismatch.");
231 std::vector<idxt> node_to_scc(cfg.
size(), -1);
232 auto nof_sccs = cfg.
SCCs(node_to_scc);
235 std::vector<int> scc_size(nof_sccs, 0);
236 for(
auto scc : node_to_scc)
239 0 <= scc && scc < nof_sccs,
"Could not determine SCC for instruction");
244 for(
size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
246 auto size = scc_size[scc_id];
250 for(
const auto &node_id : node_to_scc)
252 if(node_to_scc[node_id] == scc_id)
254 const auto &pc = cfg[node_id].PC;
267 " (assigned by the contract of ";
A base class for relations, i.e., binary predicates whose two operands have the same type.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_false() const
Return whether the expression is a constant representing false.
The Boolean constant false.
This class represents an instruction in the GOTO intermediate representation.
source_locationt & source_location_nonconst()
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
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
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
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
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc a single expression expr
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
const irep_idt & id() 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...
const irep_idt & get_function() const
void add_pragma(const irep_idt &pragma)
The symbol table base class interface.
The type of an expression, extends irept.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
void add_pragma_disable_pointer_checks(source_locationt &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.
static void append_safe_havoc_code_for_expr(const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
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 simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
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.
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK