CBMC
dfcc.cpp File Reference
+ Include dependency graph for dfcc.cpp:

Go to the source code of this file.

Functions

static std::pair< irep_idt, irep_idtparse_function_contract_pair (const irep_idt &cli_flag)
 
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...
 

Function Documentation

◆ parse_function_contract_pair()

static std::pair<irep_idt, irep_idt> parse_function_contract_pair ( const irep_idt cli_flag)
static

Definition at line 74 of file dfcc.cpp.