|
CBMC
|
This is the complete list of members for dfcc_spec_functionst, including all inherited members.
| dfcc_spec_functionst(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library) | dfcc_spec_functionst | |
| generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets) | dfcc_spec_functionst | |
| generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets) | dfcc_spec_functionst | |
| get_target_type(const exprt &expr) | dfcc_spec_functionst | protected |
| goto_model | dfcc_spec_functionst | protected |
| library | dfcc_spec_functionst | protected |
| log | dfcc_spec_functionst | protected |
| message_handler | dfcc_spec_functionst | protected |
| ns | dfcc_spec_functionst | protected |
| to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets) | dfcc_spec_functionst | |
| to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) | dfcc_spec_functionst | |
| to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets) | dfcc_spec_functionst | |
| to_spec_frees_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets) | dfcc_spec_functionst |