58 exprt decreases_clause,
61 const auto loop_head_location = loop_head->source_location();
62 const auto loop_number = loop_end->loop_number;
65 const auto &decreases_clause_exprs = decreases_clause.
operands();
69 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
132 invariant.
swap(replace_history_result.expression_after_replacement);
133 const auto &history_var_map = replace_history_result.parameter_to_history;
137 replace_history_result.history_construction;
141 const auto entered_loop =
144 id2string(loop_head_location.get_function()),
150 pre_loop_head_instrs.
add(
152 pre_loop_head_instrs.
add(
157 const auto initial_invariant_val =
160 id2string(loop_head_location.get_function()),
166 pre_loop_head_instrs.
add(
173 initial_invariant_val, invariant};
177 initial_invariant_value_assignment, pre_loop_head_instrs, mode);
184 id2string(loop_head_location.get_function()),
190 pre_loop_head_instrs.
add(
192 pre_loop_head_instrs.
add(
209 loop_head, loop_end, snapshot_instructions);
214 if(assigns_clause.
is_nil())
230 log.
debug() <<
"No loop assigns clause provided. Inferred targets: {";
232 bool ran_once =
false;
233 for(
const auto &target : to_havoc)
240 target, snapshot_instructions);
245 std::inserter(to_havoc, to_havoc.end()));
249 log.
error() <<
"Failed to infer variables being modified by the loop at "
250 << loop_head_location
251 <<
".\nPlease specify an assigns clause.\nReason:"
260 for(
const auto &target : assigns_clause.
operands())
262 to_havoc.insert(target);
275 pre_loop_head_instrs.
add(
282 const auto step_case_target =
295 "Check loop invariant before entry");
303 goto_function.body.destructive_insert(
310 const auto in_loop_havoc_block =
313 id2string(loop_head_location.get_function()),
319 pre_loop_head_instrs.
add(
321 pre_loop_head_instrs.
add(
326 pre_loop_head_instrs.
add(
333 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
346 for(
const auto &clause : decreases_clause.
operands())
348 const auto old_decreases_var =
351 id2string(loop_head_location.get_function()),
357 pre_loop_head_instrs.
add(
359 old_decreases_vars.push_back(old_decreases_var);
361 const auto new_decreases_var =
364 id2string(loop_head_location.get_function()),
370 pre_loop_head_instrs.
add(
372 new_decreases_vars.push_back(new_decreases_var);
376 if(loop_end->is_goto() && !loop_end->condition().is_true())
378 log.
error() <<
"Loop contracts are unsupported on do/while loops: "
389 if(!decreases_clause.
is_nil())
391 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
394 old_decreases_vars[i], decreases_clause_exprs[i]};
397 old_decreases_assignment, pre_loop_head_instrs, mode);
400 goto_function.body.destructive_insert(
408 goto_function.body.destructive_insert(
423 pre_loop_end_instrs.
add(
429 step_case_target, in_base_case, loop_head_location));
443 "Check that loop invariant is preserved");
449 if(!decreases_clause.
is_nil())
451 for(
size_t i = 0; i < new_decreases_vars.size(); i++)
454 new_decreases_vars[i], decreases_clause_exprs[i]};
457 new_decreases_assignment, pre_loop_end_instrs, mode);
464 new_decreases_vars, old_decreases_vars)};
466 monotonic_decreasing_assertion.add_source_location().
set_comment(
467 "Check decreases clause on loop iteration");
469 monotonic_decreasing_assertion, pre_loop_end_instrs, mode);
472 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
474 pre_loop_end_instrs.
add(
476 pre_loop_end_instrs.
add(
487 loop_end->turn_into_assume();
488 loop_end->condition_nonconst() =
boolean_negate(loop_end->condition());
490 std::set<goto_programt::targett, goto_programt::target_less_than>
494 for(
const auto &t : loop)
499 auto exit_target = t->get_target();
501 loop.contains(exit_target) ||
502 seen_targets.find(exit_target) != seen_targets.end())
505 seen_targets.insert(exit_target);
511 "Check that loop instrumentation was not truncated");
514 annotated_location));
516 pre_loop_exit_instrs.
add(
518 pre_loop_exit_instrs.
add(
520 for(
const auto &v : history_var_map)
522 pre_loop_exit_instrs.
add(
527 goto_function.body, exit_target, pre_loop_exit_instrs);
538 it.is_function_call() && it.call_function().id() == ID_symbol &&
544 it.source_location());
554 exprt &instantiated_clause,
576 constraint.
instructions.back().source_location_nonconst() = location;
577 is_fresh_update(constraint);
585 const std::string &function_str =
id2string(
function);
586 const auto &function_symbol = ns.
lookup(
function);
589 if(ns.
lookup(
"contract::" + function_str, contract_sym))
597 type == function_symbol.type,
598 "front-end should have rejected re-declarations with a different type");
609 const auto &const_target =
613 PRECONDITION(const_target->call_function().id() == ID_symbol);
628 std::optional<exprt> call_ret_opt = {};
631 bool call_ret_is_fresh_var =
false;
636 if(target->call_lhs().is_not_nil())
642 auto &lhs_expr = const_target->call_lhs();
643 call_ret_opt = lhs_expr;
644 instantiation_values.push_back(lhs_expr);
651 type.c_ensures().begin(),
652 type.c_ensures().end(),
654 return has_symbol_expr(
655 to_lambda_expr(e).where(), CPROVER_PREFIX
"return_value", true);
660 call_ret_is_fresh_var =
true;
664 "ignored_return_value",
665 const_target->source_location(),
670 call_ret_opt = fresh_sym_expr;
671 instantiation_values.push_back(fresh_sym_expr);
676 instantiation_values.push_back(
683 const auto &arguments = const_target->call_arguments();
684 instantiation_values.insert(
685 instantiation_values.end(), arguments.begin(), arguments.end());
687 const auto &mode = function_symbol.
mode;
698 for(
const auto &clause : type.c_requires())
700 auto instantiated_clause =
704 _location.
set_comment(std::string(
"Check requires clause of ")
705 .append(target_function.
c_str())
707 .append(
function.c_str()));
723 for(
auto clause : type.c_ensures())
725 auto instantiated_clause =
730 instantiated_ensures_clauses.push_back(instantiated_clause);
736 for(
auto &target : type.c_assigns())
737 targets.push_back(
to_lambda_expr(target).application(instantiation_values));
753 havocker.get_instructions(havoc_instructions);
756 if(call_ret_opt.has_value())
758 auto &call_ret = call_ret_opt.value();
759 auto &loc = call_ret.source_location();
760 auto &type = call_ret.type();
763 if(call_ret_is_fresh_var)
764 havoc_instructions.
add(
776 for(
auto &clause : instantiated_ensures_clauses)
778 if(clause.is_false())
781 std::string(
"Attempt to assume false at ")
782 .append(clause.source_location().as_string())
783 .append(
".\nPlease update ensures clause to avoid vacuity."));
799 if(call_ret_is_fresh_var)
803 target->output(mstream);
804 mstream << messaget::eom;
831 const bool may_have_loops = std::any_of(
832 goto_function.body.instructions.begin(),
833 goto_function.body.instructions.end(),
835 return instruction.is_backwards_goto();
847 "Recursive functions found during inlining");
865 struct loop_graph_nodet :
public graph_nodet<empty_edget>
869 exprt assigns_clause, invariant, decreases_clause;
875 const exprt &assigns,
877 const exprt &decreases)
881 assigns_clause(assigns),
883 decreases_clause(decreases)
889 std::list<size_t> to_check_contracts_on_children;
893 std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
897 for(
const auto &loop_head_and_content : natural_loops.
loop_map)
899 const auto &loop_body = loop_head_and_content.second;
901 if(loop_body.size() <= 1)
904 auto loop_head = loop_head_and_content.first;
905 auto loop_end = loop_head;
908 for(
const auto &t : loop_body)
911 t->is_goto() && t->get_target() == loop_head &&
912 t->location_number > loop_end->location_number)
916 if(loop_end == loop_head)
918 log.
error() <<
"Could not find end of the loop starting at: "
931 for(
const auto &i : loop_body)
934 loop_head->location_number > i->location_number ||
935 i->location_number > loop_end->location_number)
939 mstream <<
"Computed loop at " << loop_head->source_location()
940 <<
"contains an instruction beyond [loop_head, loop_end]:"
943 mstream << messaget::eom;
949 if(!loop_head_ends.emplace(loop_head, std::make_pair(loop_end, loop_body))
954 for(
auto &loop_head_end : loop_head_ends)
956 auto loop_head = loop_head_end.first;
957 auto loop_end = loop_head_end.second.first;
967 loop_end->set_target(loop_head);
969 exprt assigns_clause =
970 static_cast<const exprt &
>(loop_end->condition().find(ID_C_spec_assigns));
972 loop_end->condition().find(ID_C_spec_loop_invariant));
973 exprt decreases_clause =
static_cast<const exprt &
>(
974 loop_end->condition().find(ID_C_spec_decreases));
984 <<
" does not have an invariant in its contract.\n"
985 <<
"Hence, a default invariant ('true') is being used.\n"
986 <<
"This choice is sound, but verification may fail"
987 <<
" if it is be too weak to prove the desired properties."
994 if(decreases_clause.
is_nil())
998 <<
" does not have a decreases clause in its contract.\n"
999 <<
"Termination of this loop will not be verified."
1004 const auto idx = loop_nesting_graph.
add_node(
1005 loop_head_end.second.second,
1014 decreases_clause.
is_nil())
1017 to_check_contracts_on_children.push_back(idx);
1020 for(
size_t outer = 0; outer < loop_nesting_graph.
size(); ++outer)
1022 for(
size_t inner = 0; inner < loop_nesting_graph.
size(); ++inner)
1027 if(loop_nesting_graph[outer].content.contains(
1028 loop_nesting_graph[inner].head_target))
1030 if(!loop_nesting_graph[outer].content.contains(
1031 loop_nesting_graph[inner].end_target))
1034 <<
"Overlapping loops at:\n"
1035 << loop_nesting_graph[outer].head_target->source_location()
1037 << loop_nesting_graph[inner].head_target->source_location()
1038 <<
"\nLoops must be nested or sequential for contracts to be "
1042 loop_nesting_graph.
add_edge(inner, outer);
1048 while(!to_check_contracts_on_children.empty())
1050 const auto loop_idx = to_check_contracts_on_children.front();
1051 to_check_contracts_on_children.pop_front();
1053 const auto &loop_node = loop_nesting_graph[loop_idx];
1055 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1056 loop_node.decreases_clause.is_nil())
1060 <<
" does not have contracts, but an enclosing loop does.\n"
1061 <<
"Please provide contracts for this loop, or unwind it first."
1067 to_check_contracts_on_children.push_back(child_idx);
1072 for(
const auto &idx : loop_nesting_graph.
topsort())
1074 const auto &loop_node = loop_nesting_graph[idx];
1076 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1077 loop_node.decreases_clause.is_nil())
1104 loop_node.head_target,
1105 loop_node.end_target,
1106 updated_loops.
loop_map[loop_node.head_target],
1107 loop_node.assigns_clause,
1108 loop_node.invariant,
1109 loop_node.decreases_clause,
1121 "Function '" +
id2string(
function) +
"'must exist in the goto program");
1123 const auto &goto_function = function_obj->second;
1124 auto &function_body = function_obj->second.body;
1156 "Loops remain in function '" +
id2string(
function) +
1157 "', assigns clause checking instrumentation cannot be applied.");
1160 auto instruction_it = function_body.instructions.begin();
1164 function_body, instruction_it, snapshot_static_locals);
1173 instantiation_values.push_back(
exprt{ID_nil, function_type.
return_type()});
1174 for(
const auto ¶m : function_type.
parameters())
1176 instantiation_values.push_back(
1177 ns.
lookup(param.get_identifier()).symbol_expr());
1183 to_lambda_expr(target).application(instantiation_values), payload);
1189 for(
const auto ¶m : function_type.
parameters())
1193 ns.
lookup(param.get_identifier()).symbol_expr(), payload);
1202 function_body, instruction_it, function_body.instructions.end());
1212 std::stringstream ss;
1220 "Function to replace must exist in the program.");
1227 sl.
set_file(
"instrumented for code contracts");
1230 symbolt mangled_sym = *original_sym;
1231 mangled_sym.
name = mangled;
1236 mangled_found.second,
1237 "There should be no existing function called " + ss.str() +
1238 " in the symbol table because that name is a mangled name");
1244 "There should be no function called " +
id2string(
function) +
1245 " in the function map because that function should have had its"
1251 "There should be a function called " + ss.str() +
1252 " in the function map because we inserted a fresh goto-program"
1253 " with that mangled name");
1292 std::optional<code_returnt> return_stmt;
1296 code_type.return_type(),
1300 function_symbol.
mode,
1308 instantiation_values.push_back(
r);
1312 goto_functionst::function_mapt::iterator f_it =
1317 for(
const auto ¶meter : gf.parameter_identifiers)
1322 parameter_symbol.
type,
1326 parameter_symbol.
mode,
1331 p, parameter_symbol.
symbol_expr(), source_location));
1335 instantiation_values.push_back(p);
1344 for(
const auto &clause : code_type.c_requires())
1346 auto instantiated_clause =
1351 std::string(
"Attempt to assume false at ")
1352 .append(clause.source_location().as_string())
1353 .append(
".\nPlease update requires clause to avoid vacuity."));
1361 instantiated_clause,
1362 function_symbol.
mode,
1364 visitor.update_requires(c_requires);
1372 for(
auto clause : code_type.c_ensures())
1374 auto instantiated_clause =
1379 instantiated_ensures_clauses.push_back(instantiated_clause);
1386 for(
auto &clause : instantiated_ensures_clauses)
1395 function_symbol.
mode,
1396 [&visitor](
goto_programt &ensures) { visitor.update_ensures(ensures); },
1404 return_stmt.value().return_value(), source_location));
1418 const std::set<std::string> &functions)
const
1420 for(
const auto &
function : functions)
1427 "Function '" +
function +
"' was not found in the GOTO program.");
1434 if(to_replace.empty())
1445 if(ins->is_function_call())
1447 if(ins->call_function().id() != ID_symbol)
1452 auto found = std::find(
1453 to_replace.begin(), to_replace.end(),
id2string(called_function));
1454 if(found == to_replace.end())
1458 goto_function.first,
1459 ins->source_location(),
1460 goto_function.second.body,
1473 const std::set<std::string> &to_exclude_from_nondet_init)
1478 log.
status() <<
"Adding nondeterministic initialization "
1479 "of static/global variables."
1497 auto &goto_function = goto_function_entry.second;
1498 bool is_in_loop_havoc_block =
false;
1500 unsigned loop_number_of_loop_havoc = 0;
1502 goto_function.body.instructions.begin();
1503 it_instr != goto_function.body.instructions.end();
1516 const auto &assign_lhs =
1517 expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
1519 id2string(assign_lhs->get_identifier()),
1532 is_in_loop_havoc_block = it_instr->assign_rhs() ==
true_exprt();
1533 const auto &assign_lhs =
1534 expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
1536 id2string(assign_lhs->get_identifier()),
1542 if(is_in_loop_havoc_block && it_instr->is_assign())
1554 const std::set<std::string> &to_enforce,
1555 const std::set<std::string> &to_exclude_from_nondet_init)
1557 if(to_enforce.empty())
1564 for(
const auto &
function : to_enforce)
1567 log.
status() <<
"Adding nondeterministic initialization "
1568 "of static/global variables."
API to expression classes that are internal to the C frontend.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
A non-fatal assertion, which checks a condition then permits execution to continue.
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
void apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
void enforce_contract(const irep_idt &function)
Enforce contract of a single function.
void check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
symbol_tablet & symbol_table
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
std::unordered_set< irep_idt > summarized
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
std::list< std::string > loop_names
Name of loops we are going to unwind.
goto_functionst & goto_functions
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Store the map from instrumented instructions for loop contracts to their original loop numbers.
void add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ens...
bool unwind_transformed_loops
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
const typet & return_type() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
bool is_false() const
Return whether the expression is a constant representing false.
The Boolean constant false.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
This class represents a node in a directed graph.
A generic directed graph with a parametric node type.
std::vector< node_indext > get_predecessors(const node_indext &n) const
node_indext add_node(arguments &&... values)
void add_edge(node_indext a, node_indext b)
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Class to generate havocking instructions for target expressions of a function contract's assign claus...
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
const std::set< irep_idt > & get_recursive_call_set() const
A class that generates instrumentation for assigns clause checking.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
void instrument_instructions(goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})
Instruments a sequence of instructions with inclusion checks.
void track_static_locals_between(goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)
Searches the goto instructions reachable between the given it and end target instructions to identify...
void get_static_locals(std::insert_iterator< C > inserter) const
Inserts the detected static local symbols into a target container.
Thrown when we can't handle something in an input source file.
void add_memory_map_decl(goto_programt &program)
void update_requires(goto_programt &requires_)
void add_memory_map_dead(goto_programt &program)
void update_ensures(goto_programt &ensures)
virtual void create_declarations()
virtual void create_declarations()
exprt application(const operandst &arguments) const
void erase_locals(std::set< exprt > &exprs)
A loop, specified as a set of instructions.
source_locationt source_location
mstreamt & warning() const
mstreamt & status() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
message_handlert & get_message_handler()
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().
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() const
const irep_idt & get_line() const
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
The Boolean constant true.
static const code_with_contract_typet & get_contract(const irep_idt &function, const namespacet &ns)
static void generate_contract_constraints(symbol_tablet &symbol_table, goto_convertt &converter, exprt &instantiated_clause, const irep_idt &mode, const std::function< void(goto_programt &)> &is_fresh_update, goto_programt &program, const source_locationt &location)
This function generates instructions for all contract constraint, i.e., assumptions and assertions ba...
static void throw_on_unsupported(const goto_programt &program)
Throws an exception if a contract uses unsupported constructs like:
Verify and use annotated invariants and pre/post-conditions.
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
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.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Havoc function assigns clauses.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Field-insensitive, location-sensitive may-alias analysis.
natural_loops_mutablet::natural_loopt loopt
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Predicates to specify memory footprint in function contracts.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#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,...
#define PRECONDITION(CONDITION)
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 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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
A total order over targett and const_targett.
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
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 widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
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...
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
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 IN_LOOP_HAVOC_BLOCK