Dynamic Frame Condition Checking (DFCC)
Collaboration diagram for Dynamic Frame Condition Checking (DFCC):Files | |
| file | dfcc.h |
| Main class orchestrating the the whole program transformation for function contracts with Dynamic Frame Condition Checking (DFCC) | |
Classes | |
| class | dfcct |
| Entry point into the contracts transformation. More... | |
Functions | |
| 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 loop_contract_configt loop_contract_config, 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 approach. More... | |
Detailed Description
Function Documentation
◆ dfcc()
| 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 loop_contract_configt | loop_contract_config, | ||
| 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 approach.
- Precondition
- This function requires that the contract associated to function
fooexists in the symbol table as symbolcontract::foo.
- Parameters
-
options CLI options (used to lookup options for language config when re-defining the model's entry point) goto_model GOTO model to transform harness_id proof harness name, must be the entry point of the model to_check function to check against its contract allow_recursive_calls Allow the checked function to be recursive to_replace set of functions to replace with their contract loop_contract_config configuration for applying loop contracts to_exclude_from_nondet_static set of symbols to exclude when havocing static program symbols. message_handler used for debug/warning/error messages
