29 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
30 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H
55 #define FLAG_DFCC "dfcc"
56 #define OPT_DFCC "(" FLAG_DFCC "):"
59 " {y--dfcc} {uharness} \t " \
60 "activate dynamic frame condition checking for contracts using the given " \
61 "harness as entry point\n"
63 #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
64 #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
65 #define HELP_ENFORCE_CONTRACT_REC \
66 " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t " \
67 "wrap {ufunction} with an assertion of the contract and assume recursive " \
69 "{ufunction} satisfy the contract\n"
80 std::string
what()
const override;
109 const std::optional<irep_idt> &to_check,
110 const bool allow_recursive_calls,
111 const std::set<irep_idt> &to_replace,
112 const bool apply_loop_contracts,
113 const bool unwind_transformed_loops,
114 const std::set<std::string> &to_exclude_from_nondet_static,
142 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
143 const bool allow_recursive_calls,
144 const std::map<irep_idt, irep_idt> &to_replace,
145 const bool apply_loop_contracts,
146 const bool unwind_transformed_loops,
147 const std::set<std::string> &to_exclude_from_nondet_static,
170 const std::optional<std::pair<irep_idt, irep_idt>> &
to_check,
172 const std::map<irep_idt, irep_idt> &
to_replace,
207 const std::optional<std::pair<irep_idt, irep_idt>> &
to_check;
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Base class for exceptions thrown in the cprover project.
std::string reason
The reason this exception was generated.
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
A contract is represented by a function declaration or definition with contract clauses attached to i...
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
Entry point into the contracts transformation.
std::set< irep_idt > function_pointer_contracts
std::set< irep_idt > pure_contract_symbols
dfcc_spec_functionst spec_functions
void instrument_harness_function()
void instrument_other_functions()
dfcct(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< std::pair< irep_idt, irep_idt >> &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
Class constructor.
void reinitialize_model()
Re-initialise the GOTO model.
const std::set< std::string > & to_exclude_from_nondet_static
void link_model_and_load_dfcc_library()
dfcc_swap_and_wrapt swap_and_wrap
dfcc_lift_memory_predicatest memory_predicates
void wrap_checked_function()
void lift_memory_predicates()
const dfcc_loop_contract_modet loop_contract_mode
const std::optional< std::pair< irep_idt, irep_idt > > & to_check
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
std::size_t max_assigns_clause_size
Tracks the maximum number of targets in any assigns clause handled in the transformation (used to spe...
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
dfcc_instrumentt instrument
void wrap_replaced_functions()
message_handlert & message_handler
const irep_idt & harness_id
dfcc_contract_clauses_codegent contract_clauses_codegen
const bool allow_recursive_calls
std::set< irep_idt > other_symbols
dfcc_contract_handlert contract_handler
const std::map< irep_idt, irep_idt > & to_replace
void partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
Partitions the function symbols of the symbol table into pure contracts and other function symbols sy...
void wrap_discovered_function_pointer_contracts()
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Exception thrown for bad function/contract specification pairs passed on the CLI.
invalid_function_contract_pair_exceptiont(std::string reason, std::string correct_format="")
std::string what() const override
A human readable description of what went wrong.
std::string correct_format
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...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Specialisation of dfcc_contract_handlert for contracts.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Given a function_id and contract_id, swaps its body to a function with a fresh mangled name,...
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...