cprover
|
#include <goto_model.h>
Public Member Functions | |
void | clear () |
void | output (std::ostream &out) |
goto_modelt () | |
goto_modelt (const goto_modelt &)=delete | |
goto_modelt & | operator= (const goto_modelt &)=delete |
goto_modelt (goto_modelt &&other) | |
goto_modelt & | operator= (goto_modelt &&other) |
Public Attributes | |
symbol_tablet | symbol_table |
goto_functionst | goto_functions |
Definition at line 22 of file goto_model.h.
|
inline |
Definition at line 40 of file goto_model.h.
|
delete |
|
inline |
Definition at line 54 of file goto_model.h.
|
inline |
Definition at line 28 of file goto_model.h.
References symbol_tablet::clear(), goto_functions_templatet< bodyT >::clear(), goto_functions, and symbol_table.
|
delete |
|
inline |
Definition at line 60 of file goto_model.h.
References goto_functions, and symbol_table.
|
inline |
Definition at line 34 of file goto_model.h.
References goto_functions, goto_functions_templatet< bodyT >::output(), and symbol_table.
goto_functionst goto_modelt::goto_functions |
Definition at line 26 of file goto_model.h.
Referenced by adjust_float_expressions(), clear(), compute_called_functions(), show_goto_functions_jsont::convert(), goto_difft::convert_function(), goto_analyzer_parse_optionst::doit(), symex_parse_optionst::doit(), goto_diff_parse_optionst::get_goto_program(), goto_check(), goto_convert(), goto_function_inline(), goto_inline(), goto_partial_inline(), initialize_goto_model(), label_properties(), link_to_library(), list_functions(), make_assertions_false(), mm_io(), show_goto_functions_jsont::operator()(), syntactic_difft::operator()(), ai_baset::operator()(), operator=(), output(), ai_baset::output(), goto_difft::output_functions(), ai_baset::output_json(), ai_baset::output_xml(), parameter_assignments(), goto_diff_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), read_goto_binary(), read_object_and_link(), remove_asm(), remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_returns(), remove_vector(), remove_virtual_functions(), rewrite_union(), set_properties(), symex_parse_optionst::set_properties(), show_goto_functions(), show_loop_ids(), show_properties(), slice_global_inits(), taint_analysis(), and unreachable_instructions().
symbol_tablet goto_modelt::symbol_table |
Definition at line 25 of file goto_model.h.
Referenced by adjust_float_expressions(), clear(), goto_analyzer_parse_optionst::doit(), symex_parse_optionst::doit(), goto_diff_parse_optionst::get_goto_program(), symex_parse_optionst::get_test(), goto_check(), goto_convert(), goto_function_inline(), goto_inline(), goto_partial_inline(), initialize_goto_model(), link_to_library(), list_functions(), mm_io(), ai_baset::operator()(), operator=(), output(), ai_baset::output(), ai_baset::output_json(), ai_baset::output_xml(), parameter_assignments(), goto_diff_parse_optionst::process_goto_program(), read_goto_binary(), read_object_and_link(), remove_asm(), remove_complex(), remove_exceptions(), remove_function_pointers(), remove_instanceof(), remove_returns(), remove_vector(), remove_virtual_functions(), symex_parse_optionst::report_cover(), rewrite_union(), symex_parse_optionst::show_counterexample(), show_goto_functions(), show_properties(), show_symbol_table_plain(), taint_analysis(), and unreachable_instructions().