14#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
15#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
20#include <unordered_set>
34#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
35#define HELP_LOOP_CONTRACTS \
36 " --apply-loop-contracts\n" \
37 " check and use loop contracts when provided\n"
39#define FLAG_REPLACE_CALL "replace-call-with-contract"
40#define HELP_REPLACE_CALL \
41 " --replace-call-with-contract <fun>\n" \
42 " replace calls to fun with fun's contract\n"
44#define FLAG_ENFORCE_CONTRACT "enforce-contract"
45#define HELP_ENFORCE_CONTRACT \
46 " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
209 const exprt &expression,
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 ...
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...
code_contractst(goto_modelt &goto_model, messaget &log)
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()
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.
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A class that generates instrumentation for assigns clause checking.
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...
Replace expression or type symbols by an expression or type, respectively.
Goto Programs with Functions.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
API to expression classes for Pointers.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)