CBMC
|
This is the complete list of members for dfcct, including all inherited members.
allow_recursive_calls | dfcct | protected |
check_transform_goto_model_preconditions() | dfcct | protected |
contract_clauses_codegen | dfcct | protected |
contract_handler | dfcct | protected |
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 loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static) | dfcct | |
function_pointer_contracts | dfcct | protected |
goto_model | dfcct | protected |
harness_id | dfcct | protected |
instrument | dfcct | protected |
instrument_harness_function() | dfcct | protected |
instrument_other_functions() | dfcct | protected |
library | dfcct | protected |
lift_memory_predicates() | dfcct | protected |
link_model_and_load_dfcc_library() | dfcct | protected |
log | dfcct | protected |
loop_contract_config | dfcct | protected |
max_assigns_clause_size | dfcct | protected |
memory_predicates | dfcct | protected |
message_handler | dfcct | protected |
ns | dfcct | protected |
options | dfcct | protected |
other_symbols | dfcct | protected |
partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols) | dfcct | protected |
pure_contract_symbols | dfcct | protected |
reinitialize_model() | dfcct | protected |
spec_functions | dfcct | protected |
swap_and_wrap | dfcct | protected |
to_check | dfcct | protected |
to_exclude_from_nondet_static | dfcct | protected |
to_replace | dfcct | protected |
transform_goto_model() | dfcct | |
wrap_checked_function() | dfcct | protected |
wrap_discovered_function_pointer_contracts() | dfcct | protected |
wrap_replaced_functions() | dfcct | protected |