CBMC
lazy_goto_modelt Member List

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

add_language_file(const std::string &filename)lazy_goto_modeltinline
can_generate_function_bodyt typedeflazy_goto_modelt
can_produce_function(const irep_idt &id) const overridelazy_goto_modeltvirtual
driver_program_can_generate_function_bodylazy_goto_modeltprivate
driver_program_generate_function_bodylazy_goto_modeltprivate
finalize()lazy_goto_modeltprivate
from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)lazy_goto_modeltinlinestatic
generate_function_bodyt typedeflazy_goto_modelt
get_goto_function(const irep_idt &id) overridelazy_goto_modeltinlinevirtual
get_goto_functions() const overridelazy_goto_modeltinlinevirtual
get_symbol_table() const overridelazy_goto_modeltinlinevirtual
goto_functionslazy_goto_modeltprivate
goto_modellazy_goto_modeltprivate
initialize(const std::vector< std::string > &files, const optionst &options)lazy_goto_modelt
language_fileslazy_goto_modeltprivate
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_modeltexplicit
lazy_goto_modelt(lazy_goto_modelt &&other)lazy_goto_modelt
load_all_functions() constlazy_goto_modelt
message_handlerlazy_goto_modeltprivate
operator=(lazy_goto_modelt &&other)lazy_goto_modeltinline
post_process_functionlazy_goto_modeltprivate
post_process_functionslazy_goto_modeltprivate
post_process_functionst typedeflazy_goto_modelt
post_process_functiont typedeflazy_goto_modelt
process_whole_model_and_freeze(lazy_goto_modelt &&model)lazy_goto_modeltinlinestatic
symbol_tablelazy_goto_modelt
validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const overridelazy_goto_modeltinlinevirtual
~abstract_goto_modelt()abstract_goto_modeltinlinevirtual