CBMC
|
This is the complete list of members for lazy_goto_modelt, including all inherited members.
add_language_file(const std::string &filename) | lazy_goto_modelt | inline |
can_generate_function_bodyt typedef | lazy_goto_modelt | |
can_produce_function(const irep_idt &id) const override | lazy_goto_modelt | virtual |
driver_program_can_generate_function_body | lazy_goto_modelt | private |
driver_program_generate_function_body | lazy_goto_modelt | private |
finalize() | lazy_goto_modelt | private |
from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler) | lazy_goto_modelt | inlinestatic |
generate_function_bodyt typedef | lazy_goto_modelt | |
get_goto_function(const irep_idt &id) override | lazy_goto_modelt | inlinevirtual |
get_goto_functions() const override | lazy_goto_modelt | inlinevirtual |
get_symbol_table() const override | lazy_goto_modelt | inlinevirtual |
goto_functions | lazy_goto_modelt | private |
goto_model | lazy_goto_modelt | private |
initialize(const std::vector< std::string > &files, const optionst &options) | lazy_goto_modelt | |
language_files | lazy_goto_modelt | private |
lazy_goto_modelt(post_process_functiont post_process_function, post_process_functionst post_process_functions, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler) | lazy_goto_modelt | explicit |
lazy_goto_modelt(lazy_goto_modelt &&other) | lazy_goto_modelt | |
load_all_functions() const | lazy_goto_modelt | |
message_handler | lazy_goto_modelt | private |
operator=(lazy_goto_modelt &&other) | lazy_goto_modelt | inline |
post_process_function | lazy_goto_modelt | private |
post_process_functions | lazy_goto_modelt | private |
post_process_functionst typedef | lazy_goto_modelt | |
post_process_functiont typedef | lazy_goto_modelt | |
process_whole_model_and_freeze(lazy_goto_modelt &&model) | lazy_goto_modelt | inlinestatic |
symbol_table | lazy_goto_modelt | |
validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override | lazy_goto_modelt | inlinevirtual |
~abstract_goto_modelt() | abstract_goto_modelt | inlinevirtual |