cprover
|
#include <goto_model.h>
Public Member Functions | |
void | clear () |
void | output (std::ostream &out) const |
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) |
void | unload (const irep_idt &name) |
const goto_functionst & | get_goto_functions () const override |
Accessor to get a raw goto_functionst. More... | |
const symbol_tablet & | get_symbol_table () const override |
Accessor to get the symbol table. More... | |
const goto_functionst::goto_functiont & | get_goto_function (const irep_idt &id) override |
Get a GOTO function by name, or throw if no such function exists. More... | |
bool | can_produce_function (const irep_idt &id) const override |
Determines if this model can produce a body for the given function. More... | |
![]() | |
virtual | ~abstract_goto_modelt () |
Public Attributes | |
symbol_tablet | symbol_table |
Symbol table. More... | |
goto_functionst | goto_functions |
GOTO functions. More... | |
Definition at line 24 of file goto_model.h.
|
inline |
Definition at line 46 of file goto_model.h.
|
delete |
|
inline |
Definition at line 60 of file goto_model.h.
|
inlineoverridevirtual |
Determines if this model can produce a body for the given function.
id | function ID to query |
Implements abstract_goto_modelt.
Definition at line 93 of file goto_model.h.
References goto_functionst::function_map, and goto_functions.
|
inline |
Definition at line 34 of file goto_model.h.
References goto_functionst::clear(), symbol_tablet::clear(), goto_functions, and symbol_table.
|
inlineoverridevirtual |
Get a GOTO function by name, or throw if no such function exists.
May have side-effects on the GOTO function map provided by get_goto_functions, or the symbol table returned by get_symbol_table, so iterators pointing into either may be invalidated.
id | function to get |
Implements abstract_goto_modelt.
Definition at line 87 of file goto_model.h.
References goto_functionst::function_map, and goto_functions.
Referenced by instrument_cover_goals().
|
inlineoverridevirtual |
Accessor to get a raw goto_functionst.
Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.
Implements abstract_goto_modelt.
Definition at line 77 of file goto_model.h.
References goto_functions.
|
inlineoverridevirtual |
Accessor to get the symbol table.
Concurrent use of get_goto_function may invalidate iterators or otherwise surprise users by modifying the map underneath them, so this should only be used to lend a reference to code that cannot also call get_goto_function.
Implements abstract_goto_modelt.
Definition at line 82 of file goto_model.h.
References symbol_table.
|
delete |
|
inline |
Definition at line 66 of file goto_model.h.
References goto_functions, and symbol_table.
|
inline |
Definition at line 40 of file goto_model.h.
References goto_functions, goto_functionst::output(), and symbol_table.
|
inline |
Definition at line 73 of file goto_model.h.
References goto_functions, and goto_functionst::unload().
goto_functionst goto_modelt::goto_functions |
GOTO functions.
Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.
Definition at line 32 of file goto_model.h.
Referenced by accelerate_functions(), add_uninitialized_locals_assertions(), adjust_float_expressions(), branch(), janalyzer_parse_optionst::build_analyzer(), goto_analyzer_parse_optionst::build_analyzer(), can_produce_function(), custom_bitvector_analysist::check(), clear(), code_contracts(), collect_eloc(), compute_called_functions(), compute_called_functions_from_ai(), concurrency(), constant_propagator_ait::constant_propagator_ait(), goto_difft::convert_function_json(), convert_nondet(), document_properties_html(), document_properties_latex(), goto_instrument_parse_optionst::doit(), full_slicer(), function_enter(), function_exit(), generate_function_bodies(), get_goto_function(), get_goto_functions(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), goto_check(), goto_convert(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_partial_inline(), havoc_loops(), initialize_goto_model(), escape_analysist::instrument(), instrument_cover_goals(), goto_instrument_parse_optionst::instrument_goto_program(), instrument_preconditions(), interpreter(), interrupt(), interval_analysis(), is_threadedt::is_threadedt(), k_induction(), label_properties(), link_goto_model(), link_to_library(), list_calls_and_arguments(), list_functions(), list_undefined_functions(), make_assertions_false(), mm_io(), mmio(), model_argc_argv(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), points_tot::operator()(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), goto_unwindt::operator()(), ai_baset::operator()(), operator=(), dott::output(), output(), ai_baset::output(), goto_difft::output_function(), ai_baset::output_json(), ai_baset::output_xml(), parameter_assignments(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), print_global_state_size(), print_path_lengths(), jbmc_parse_optionst::process_goto_functions(), clobber_parse_optionst::process_goto_program(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), cbmc_parse_optionst::process_goto_program(), janalyzer_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), property_slicer(), race_check(), reachability_slicer(), read_goto_binary(), read_object_and_link(), remove_asm(), remove_complex(), remove_exceptions(), remove_function(), remove_function_pointers(), remove_instanceof(), remove_java_new(), remove_pointers(), remove_returns(), remove_skip(), remove_unreachable(), remove_unused_functions(), remove_vector(), remove_virtual_functions(), replace_java_nondet(), restore_returns(), rewrite_union(), set_properties(), show_call_sequences(), show_goto_functions(), show_locations(), show_loop_ids(), show_natural_loops(), show_properties(), show_uninitialized(), show_value_sets(), skip_loops(), slice_global_inits(), stack_depth(), static_simplifier(), static_unreachable_instructions(), static_verifier(), string_abstraction(), string_instrumentation(), taint_analysis(), thread_exit_instrumentation(), undefined_function_abort_path(), unload(), unreachable_instructions(), weak_memory(), and write_goto_binary().
symbol_tablet goto_modelt::symbol_table |
Symbol table.
Direct access is deprecated; use the abstract_goto_modelt interface instead if possible.
Definition at line 29 of file goto_model.h.
Referenced by cover_instrumenterst::add_from_criterion(), add_uninitialized_locals_assertions(), adjust_float_expressions(), branch(), custom_bitvector_analysist::check(), clear(), code_contracts(), concurrency(), constant_propagator_ait::constant_propagator_ait(), goto_difft::convert_function_json(), convert_nondet(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), full_slicer(), function_enter(), function_exit(), generate_function_bodies(), get_cover_config(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), get_isr(), get_symbol_table(), goto_check(), goto_convert(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_partial_inline(), initialize_goto_model(), escape_analysist::instrument(), instrument_cover_goals(), goto_instrument_parse_optionst::instrument_goto_program(), instrument_preconditions(), interpreter(), interrupt(), interval_analysis(), link_goto_model(), link_to_library(), list_calls_and_arguments(), list_functions(), list_undefined_functions(), load_java_class(), mm_io(), mmio(), model_argc_argv(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), java_syntactic_difft::operator()(), syntactic_difft::operator()(), ai_baset::operator()(), operator=(), output(), ai_baset::output(), goto_difft::output_function(), ai_baset::output_json(), ai_baset::output_xml(), parameter_assignments(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), print_global_state_size(), cbmc_parse_optionst::process_goto_program(), property_slicer(), race_check(), read_goto_binary(), read_object_and_link(), remove_asm(), remove_complex(), remove_exceptions(), remove_function(), remove_function_pointers(), remove_instanceof(), remove_java_new(), remove_pointers(), remove_returns(), remove_vector(), remove_virtual_function(), remove_virtual_functions(), restore_returns(), rewrite_union(), show_goto_functions(), show_properties(), show_symbol_table(), show_symbol_table_brief(), show_uninitialized(), stack_depth(), static_simplifier(), static_unreachable_instructions(), static_verifier(), string_abstraction(), string_instrumentation(), taint_analysis(), unreachable_instructions(), weak_memory(), dott::write_dot_subgraph(), and write_goto_binary().