|
CBMC
|
This is the complete list of members for code_contractst, including all inherited members.
| add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest) | code_contractst | |
| add_quantified_variable(exprt &expression, const irep_idt &mode) | code_contractst | |
| apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target) | code_contractst | |
| apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function) | code_contractst | |
| apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={}) | code_contractst | |
| assert_function_pointer_obeys_contract(const function_pointer_obeys_contract_exprt &expr, const irep_idt &property_class, const irep_idt &mode, goto_programt &dest) | code_contractst | |
| assume_function_pointer_obeys_contract(const function_pointer_obeys_contract_exprt &expr, const irep_idt &mode, goto_programt &dest) | code_contractst | |
| check_all_functions_found(const std::set< std::string > &functions) const | code_contractst | |
| check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode) | code_contractst | |
| check_frame_conditions_function(const irep_idt &function) | code_contractst | |
| code_contractst(goto_modelt &goto_model, messaget &log) | code_contractst | inline |
| converter | code_contractst | protected |
| create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode) | code_contractst | |
| enforce_contract(const irep_idt &function) | code_contractst | |
| enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={}) | code_contractst | |
| get_goto_functions() | code_contractst | |
| get_symbol_table() | code_contractst | |
| goto_functions | code_contractst | protected |
| goto_model | code_contractst | protected |
| log | code_contractst | protected |
| ns | code_contractst | |
| replace_calls(const std::set< std::string > &to_replace) | code_contractst | |
| replace_history_parameter(exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id) | code_contractst | |
| summarized | code_contractst | protected |
| symbol_table | code_contractst | protected |