67 if(message.find(
"recursion is ignored on call") != std::string::npos)
81 void print(
unsigned level,
const std::string &message)
override
104 const std::string &message,
132 std::string
command(
unsigned i)
const override
150 for(
const auto &t : loop)
152 t->is_goto() && t->get_target() == loop_head &&
153 t->location_number > loop_end->location_number)
157 auto assigns_clause =
static_cast<const exprt &
>(
158 loop_end->get_condition().find(ID_C_spec_assigns));
159 auto invariant =
static_cast<const exprt &
>(
160 loop_end->get_condition().find(ID_C_spec_loop_invariant));
161 auto decreases_clause =
static_cast<const exprt &
>(
162 loop_end->get_condition().find(ID_C_spec_decreases));
164 if(invariant.is_nil())
166 if(decreases_clause.is_nil() && assigns_clause.is_nil())
173 <<
" does not have an invariant, but has other clauses"
174 <<
" specified in its contract.\n"
175 <<
"Hence, a default invariant ('true') is being used to prove those."
186 const auto &decreases_clause_exprs = decreases_clause.operands();
190 std::vector<symbol_exprt> old_decreases_vars;
191 std::vector<symbol_exprt> new_decreases_vars;
216 const auto &invariant_expr = [&]() {
217 auto invariant_copy = invariant;
221 return invariant_copy;
226 std::map<exprt, exprt> parameter2history;
230 loop_head->source_location(),
242 generated_code.
instructions.back().source_location_nonconst().set_comment(
243 "Check loop invariant before entry");
269 if(assigns_clause.is_nil())
279 log.
debug() <<
"No loop assigns clause provided. Inferred targets {";
281 bool ran_once =
false;
282 for(
const auto &target : to_havoc)
289 target, snapshot_instructions);
292 <<
"}. Please specify an assigns clause if verification fails."
297 log.
error() <<
"Failed to infer variables being modified by the loop at "
299 <<
".\nPlease specify an assigns clause.\nReason:"
308 for(
const auto &target : assigns_clause.operands())
310 to_havoc.insert(target);
319 goto_function.body, loop_head, snapshot_instructions);
329 instrument_spec_assigns,
338 loop_head->source_location(), generated_code);
342 if(assigns_clause.is_nil())
349 goto_function.body, loop_head, generated_code);
369 for(
const auto &clause : decreases_clause.operands())
371 const auto old_decreases_var =
373 clause.type(), loop_head->source_location(), mode,
symbol_table)
376 old_decreases_var, loop_head->source_location()));
377 old_decreases_vars.push_back(old_decreases_var);
379 const auto new_decreases_var =
381 clause.type(), loop_head->source_location(), mode,
symbol_table)
384 new_decreases_var, loop_head->source_location()));
385 new_decreases_vars.push_back(new_decreases_var);
389 if(loop_end->is_goto() && !loop_end->get_condition().is_true())
391 log.
error() <<
"Loop contracts are unsupported on do/while loops: "
415 const auto head_loc = loop_head->source_location();
416 while(loop_head->source_location() == head_loc ||
417 loop_head->source_location().get_function() != head_loc.get_function())
422 auto loop_body = loop_head;
427 if(!decreases_clause.is_nil())
429 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
431 code_assignt old_decreases_assignment{old_decreases_vars[i],
432 decreases_clause_exprs[i]};
434 loop_head->source_location();
438 goto_function.body.destructive_insert(
449 generated_code.
instructions.back().source_location_nonconst().set_comment(
450 "Check that loop invariant is preserved");
455 if(!decreases_clause.is_nil())
457 for(
size_t i = 0; i < new_decreases_vars.size(); i++)
459 code_assignt new_decreases_assignment{new_decreases_vars[i],
460 decreases_clause_exprs[i]};
462 loop_head->source_location();
471 new_decreases_vars, old_decreases_vars)};
473 loop_head->source_location();
475 monotonic_decreasing_assertion, generated_code, mode);
476 generated_code.
instructions.back().source_location_nonconst().set_comment(
477 "Check decreases clause on loop iteration");
480 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
483 old_decreases_vars[i], loop_head->source_location()));
485 new_decreases_vars[i], loop_head->source_location()));
495 loop_end->turn_into_assume();
496 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
500 const exprt &expression,
504 if(expression.
id() == ID_not || expression.
id() == ID_typecast)
511 if(expression.
id() == ID_notequal || expression.
id() == ID_implies)
519 if(expression.
id() == ID_if)
523 const auto &if_expression =
to_if_expr(expression);
528 if(expression.
id() == ID_and || expression.
id() == ID_or)
533 for(
const auto &operand : multi_ary_expression.operands())
538 else if(expression.
id() == ID_exists || expression.
id() == ID_forall)
543 for(
const auto &quantified_variable : quantifier_expression.variables())
545 const auto &quantified_symbol =
to_symbol_expr(quantified_variable);
549 quantified_symbol.type(),
550 quantified_symbol.source_location(),
556 quantified_symbol.get_identifier(), quantified_symbol.type());
567 std::map<exprt, exprt> ¶meter2history,
576 op, parameter2history, location, mode, history,
id);
579 if(expr.
id() == ID_old || expr.
id() == ID_loop_entry)
583 const auto &
id = parameter.
id();
585 id == ID_dereference ||
id == ID_member ||
id == ID_symbol ||
586 id == ID_ptrmember ||
id == ID_constant ||
id == ID_typecast)
588 auto it = parameter2history.find(parameter);
590 if(it == parameter2history.end())
594 const auto skip_target =
605 parameter2history[parameter] = tmp_symbol;
627 expr = parameter2history[parameter];
631 log.
error() <<
"Tracking history of " << parameter.id()
638std::pair<goto_programt, goto_programt>
644 std::map<exprt, exprt> parameter2history;
649 expression, parameter2history, location, mode, history, ID_old);
658 return std::make_pair(std::move(ensures_program), std::move(history));
667 const auto &const_target =
671 PRECONDITION(const_target->call_function().id() == ID_symbol);
681 auto assigns_clause = type.assigns();
694 bool call_ret_is_fresh_var =
false;
699 if(target->call_lhs().is_not_nil())
705 auto &lhs_expr = const_target->call_lhs();
706 call_ret_opt = lhs_expr;
708 common_replace.
insert(ret_val, lhs_expr);
720 call_ret_is_fresh_var =
true;
724 "ignored_return_value",
725 const_target->source_location(),
731 common_replace.
insert(ret_val, fresh_sym_expr);
732 call_ret_opt = fresh_sym_expr;
738 const auto &arguments = const_target->call_arguments();
739 auto a_it = arguments.begin();
740 for(
auto p_it = type.parameters().begin();
741 p_it != type.parameters().end() && a_it != arguments.end();
744 if(!p_it->get_identifier().empty())
747 common_replace.
insert(p, *a_it);
768 assertion.
instructions.back().source_location_nonconst() =
769 requires.source_location();
770 assertion.
instructions.back().source_location_nonconst().set_comment(
771 "Check requires clause");
772 assertion.
instructions.back().source_location_nonconst().set_property_class(
780 std::pair<goto_programt, goto_programt> ensures_pair;
781 if(!ensures.is_false())
790 ensures.source_location(),
801 for(
auto &target : assigns_clause)
803 common_replace(targets);
809 if(!assigns_clause.empty())
824 if(call_ret_opt.has_value())
826 auto &call_ret = call_ret_opt.value();
827 auto &loc = call_ret.source_location();
828 auto &type = call_ret.type();
831 if(call_ret_is_fresh_var)
832 havoc_instructions.
add(
836 auto target = havoc_instructions.
add(
838 target->code_nonconst().add_source_location() = loc;
846 if(!ensures.is_false())
853 if(call_ret_is_fresh_var)
874 const bool may_have_loops = std::any_of(
875 goto_function.body.instructions.begin(),
876 goto_function.body.instructions.end(),
878 return instruction.is_backwards_goto();
890 "Recursive functions found during inlining");
908 struct loop_graph_nodet :
public graph_nodet<empty_edget>
916 loop_graph_nodet(targett t,
loopt l) : target(t), loop(l)
922 for(
const auto &loop : natural_loops.
loop_map)
923 loop_nesting_graph.
add_node(loop.first, loop.second);
925 for(
size_t outer = 0; outer < loop_nesting_graph.
size(); ++outer)
927 for(
size_t inner = 0; inner < loop_nesting_graph.
size(); ++inner)
932 if(loop_nesting_graph[outer].loop.contains(
933 loop_nesting_graph[inner].target))
934 loop_nesting_graph.
add_edge(outer, inner);
940 for(
const auto &idx : loop_nesting_graph.
topsort())
942 const auto &loop_node = loop_nesting_graph[idx];
969 auto lhs = instruction_it->assign_lhs();
970 lhs.add_source_location() = instruction_it->source_location();
973 lhs, cfg_info_opt, payload);
985 instruction_it->is_function_call(),
986 "The first argument of instrument_call_statement should always be "
989 const auto &callee_name =
992 if(callee_name ==
"malloc")
994 const auto &function_call =
996 if(function_call.lhs().is_not_nil())
1000 object.add_source_location() = function_call.source_location();
1012 else if(callee_name ==
"free")
1014 const auto &ptr = instruction_it->call_arguments().front();
1016 object.add_source_location() = instruction_it->source_location();
1018 instrument_spec_assigns
1020 object, cfg_info_opt, payload);
1028 std::vector<goto_programt::instructiont> back_gotos;
1029 std::vector<goto_programt::instructiont> malloc_calls;
1036 back_gotos.push_back(instruction);
1054 if(called_name ==
"malloc")
1056 malloc_calls.push_back(instruction);
1063 for(
auto goto_entry : back_gotos)
1065 for(
const auto &target : goto_entry.targets)
1067 for(
auto malloc_entry : malloc_calls)
1070 malloc_entry.location_number >= target->location_number &&
1071 malloc_entry.location_number < goto_entry.location_number)
1073 log.
error() <<
"Call to malloc at location "
1074 << malloc_entry.location_number <<
" falls between goto "
1075 <<
"source location " << goto_entry.location_number
1076 <<
" and it's destination at location "
1077 << target->location_number <<
". "
1078 <<
"Unable to complete instrumentation, as this malloc "
1094 log.
error() <<
"Could not find function '" << function
1095 <<
"' in goto-program; not enforcing contracts."
1100 const auto &goto_function = function_obj->second;
1101 auto &function_body = function_obj->second.body;
1105 const auto &function_with_contract =
1124 "Recursive functions found during inlining");
1134 "Loops remain in function '" +
id2string(function) +
1135 "', assigns clause checking instrumentation cannot be applied.");
1140 goto_function_orig.
copy_from(goto_function);
1145 auto instruction_it = function_body.instructions.begin();
1149 function_body, instruction_it, snapshot_static_locals);
1152 for(
auto &target : function_with_contract.assigns())
1165 ns.
lookup(param.get_identifier()).symbol_expr(), payload);
1177 function_body.instructions.
end(),
1178 instrument_spec_assigns,
1191 const auto &pragmas = target->source_location().get_pragmas();
1203 const auto &symbol_expr =
1204 expr_try_dynamic_cast<symbol_exprt>(target->assign_lhs()))
1208 ns.
lookup(symbol_expr->get_identifier()).is_parameter)
1211 if(cfg_info_opt.has_value())
1212 return !cfg_info_opt.value().is_local(symbol_expr->get_identifier());
1231 if(cfg_info_opt.has_value())
1232 return cfg_info_opt.value().is_not_local_or_dirty_local(
1233 target->decl_symbol().get_identifier());
1246 if(!cfg_info_opt.has_value())
1249 return cfg_info_opt.value().is_not_local_or_dirty_local(
1250 target->dead_symbol().get_identifier());
1259 skipt skip_parameter_assigns,
1262 while(instruction_it != instruction_end)
1268 if(cfg_info_opt.has_value())
1269 cfg_info_opt.value().step();
1278 instruction_it->is_decl() &&
1282 const auto &decl_symbol = instruction_it->decl_symbol();
1294 instruction_it->is_assign() &&
1296 instruction_it, skip_parameter_assigns,
ns, cfg_info_opt))
1299 instruction_it, body, instrument_spec_assigns, cfg_info_opt);
1301 else if(instruction_it->is_function_call())
1304 instruction_it, function, body, instrument_spec_assigns, cfg_info_opt);
1307 instruction_it->is_dead() &&
1310 const auto &symbol = instruction_it->dead_symbol();
1326 log.
warning() <<
"Found a `DEAD` variable " << symbol.get_identifier()
1327 <<
" without corresponding `DECL`, at: "
1332 instruction_it->is_other() &&
1333 instruction_it->get_other().get_statement() == ID_havoc_object)
1335 auto havoc_argument = instruction_it->get_other().operands().front();
1337 havoc_object.add_source_location() = instruction_it->source_location();
1340 havoc_object, cfg_info_opt, payload);
1346 if(cfg_info_opt.has_value())
1347 cfg_info_opt.value().step();
1358 std::stringstream ss;
1366 log.
error() <<
"Could not find function '" << function
1367 <<
"' in goto-program; not enforcing contracts."
1377 sl.
set_file(
"instrumented for code contracts");
1381 mangled_sym = *original_sym;
1382 mangled_sym.
name = mangled;
1387 mangled_found.second,
1388 "There should be no existing function called " + ss.str() +
1389 " in the symbol table because that name is a mangled name");
1395 "There should be no function called " +
id2string(function) +
1396 " in the function map because that function should have had its"
1402 "There should be a function called " + ss.str() +
1403 " in the function map because we inserted a fresh goto-program"
1404 " with that mangled name");
1424 auto assigns = code_type.assigns();
1425 auto requires =
conjunction(code_type.requires());
1458 code_type.return_type(),
1459 skip->source_location(),
1460 function_symbol.
mode,
1469 common_replace.
insert(ret_val,
r);
1473 goto_functionst::function_mapt::iterator f_it =
1478 for(
const auto ¶meter : gf.parameter_identifiers)
1483 parameter_symbol.
type,
1485 parameter_symbol.
mode,
1518 std::pair<goto_programt, goto_programt> ensures_pair;
1521 if(!ensures.is_true())
1532 assertion.add_source_location() = ensures.source_location();
1534 assertion, ensures.source_location(), function_symbol.
mode);
1535 ensures_pair.first.instructions.back()
1536 .source_location_nonconst()
1537 .set_comment(
"Check ensures clause");
1538 ensures_pair.first.instructions.back()
1539 .source_location_nonconst()
1540 .set_property_class(ID_postcondition);
1551 if(ensures.is_not_nil())
1559 return_stmt.value().return_value(), skip->source_location()));
1569 if(to_replace.empty())
1578 if(ins->is_function_call())
1580 if(ins->call_function().id() != ID_symbol)
1585 auto found = std::find(
1586 to_replace.begin(), to_replace.end(),
id2string(called_function));
1587 if(found == to_replace.end())
1591 goto_function.first,
1592 ins->source_location(),
1593 goto_function.second.body,
1618 if(to_enforce.empty())
1623 for(
const auto &function : to_enforce)
1629 log.
error() <<
"Could not find function '" << function
1630 <<
"' in goto-program; not enforcing contracts."
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Stores information about a goto function computed from its CFG, together with a target iterator into ...
A non-fatal assertion, which checks a condition then permits execution to continue.
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
std::pair< goto_programt, goto_programt > create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)
This function creates and returns an instruction that corresponds to the ensures clause.
void replace_history_parameter(exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
bool 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 apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
goto_functionst & get_goto_functions()
void apply_loop_contracts()
symbol_tablet & symbol_table
void instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the function call at instruction_it,...
void add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
std::unordered_set< irep_idt > summarized
void check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
bool check_for_looped_mallocs(const goto_programt &program)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the assignment instruction_it,...
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, const loopt &loop, const irep_idt &mode)
goto_functionst & goto_functions
skipt
Tells wether to skip or not skip an action.
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
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...
symbol_tablet & get_symbol_table()
codet representation of a function call statement.
codet representation of a "return from a function" statement.
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string::const_iterator end() const
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
A collection of goto functions.
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.
void copy_from(const goto_functiont &other)
This class represents an instruction in the GOTO intermediate representation.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_function_call() const
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.
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())
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())
This class represents a node in a directed graph.
A generic directed graph with a parametric node type.
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...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
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) const
Append goto instructions to havoc the full assigns set.
const exprt & expression() const
Decorator for message_handlert that keeps track of warnings occuring when inlining a function.
void print(unsigned level, const std::string &message) override
unsigned get_verbosity() const
void print(unsigned level, const jsont &json) override
void set_verbosity(unsigned _verbosity)
void print(unsigned level, const std::string &message, const source_locationt &location) override
void flush(unsigned i) override
void print(unsigned level, const xmlt &xml) override
inlining_decoratort(message_handlert &_wrapped)
unsigned int get_recursive_function_warnings_count()
message_handlert & wrapped
void print(unsigned level, const structured_datat &data) override
std::string command(unsigned i) const override
Create an ECMA-48 SGR (Select Graphic Rendition) command.
std::size_t get_message_count(unsigned level) const
unsigned int recursive_function_warnings_count
void parse_message(const std::string &message)
A class that generates instrumentation for assigns clause checking.
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
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_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
const irep_idt & id() const
void update_requires(goto_programt &requires)
void update_ensures(goto_programt &ensures)
virtual void create_declarations()
virtual void create_declarations()
A loop, specified as a set of instructions.
void set_verbosity(unsigned _verbosity)
virtual void print(unsigned level, const std::string &message)=0
std::size_t get_message_count(unsigned level) const
unsigned get_verbosity() const
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
virtual void flush(unsigned)=0
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & warning() 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().
Replace expression or type symbols by an expression or type, respectively.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Predicate to be used with the exprt::visit() function.
bool found_return_value()
A side_effect_exprt that returns a non-deterministically chosen value.
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
A way of representing nested key/value data.
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.
const source_locationt & source_location() const
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
bool must_track_dead(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DEAD x must be processed to upate the local write set.
bool must_check_assign(const goto_programt::const_targett &target, code_contractst::skipt skip_parameter_assigns, const namespacet ns, const optionalt< cfg_infot > cfg_info_opt)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
bool must_track_decl(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DECL x must be added to the local write set.
Verify and use annotated invariants and pre/post-conditions.
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 ...
const code_function_callt & to_code_function_call(const codet &code)
#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
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
bool is_false(const literalt &l)
bool is_true(const literalt &l)
Field-insensitive, location-sensitive bitvector analysis.
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
natural_loops_mutablet::natural_loopt loopt
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Predicates to specify memory footprint in function contracts.
nonstd::optional< T > optionalt
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#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 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 multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
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.
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...
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