CBMC
dfcct Member List

This is the complete list of members for dfcct, including all inherited members.

allow_recursive_callsdfcctprotected
check_transform_goto_model_preconditions()dfcctprotected
contract_clauses_codegendfcctprotected
contract_handlerdfcctprotected
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_contractsdfcctprotected
goto_modeldfcctprotected
harness_iddfcctprotected
instrumentdfcctprotected
instrument_harness_function()dfcctprotected
instrument_other_functions()dfcctprotected
librarydfcctprotected
lift_memory_predicates()dfcctprotected
link_model_and_load_dfcc_library()dfcctprotected
logdfcctprotected
loop_contract_configdfcctprotected
max_assigns_clause_sizedfcctprotected
memory_predicatesdfcctprotected
message_handlerdfcctprotected
nsdfcctprotected
optionsdfcctprotected
other_symbolsdfcctprotected
partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)dfcctprotected
pure_contract_symbolsdfcctprotected
reinitialize_model()dfcctprotected
spec_functionsdfcctprotected
swap_and_wrapdfcctprotected
to_checkdfcctprotected
to_exclude_from_nondet_staticdfcctprotected
to_replacedfcctprotected
transform_goto_model()dfcct
wrap_checked_function()dfcctprotected
wrap_discovered_function_pointer_contracts()dfcctprotected
wrap_replaced_functions()dfcctprotected