cprover
goto_modelt Class Reference

#include <goto_model.h>

Inheritance diagram for goto_modelt:
[legend]
Collaboration diagram for goto_modelt:
[legend]

Public Member Functions

void clear ()
 
void output (std::ostream &out) const
 
 goto_modelt ()
 
 goto_modelt (const goto_modelt &)=delete
 
goto_modeltoperator= (const goto_modelt &)=delete
 
 goto_modelt (goto_modelt &&other)
 
goto_modeltoperator= (goto_modelt &&other)
 
void unload (const irep_idt &name)
 
const goto_functionstget_goto_functions () const override
 Accessor to get a raw goto_functionst. More...
 
const symbol_tabletget_symbol_table () const override
 Accessor to get the symbol table. More...
 
const goto_functionst::goto_functiontget_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...
 
- Public Member Functions inherited from abstract_goto_modelt
virtual ~abstract_goto_modelt ()
 

Public Attributes

symbol_tablet symbol_table
 Symbol table. More...
 
goto_functionst goto_functions
 GOTO functions. More...
 

Detailed Description

Definition at line 24 of file goto_model.h.

Constructor & Destructor Documentation

◆ goto_modelt() [1/3]

goto_modelt::goto_modelt ( )
inline

Definition at line 46 of file goto_model.h.

◆ goto_modelt() [2/3]

goto_modelt::goto_modelt ( const goto_modelt )
delete

◆ goto_modelt() [3/3]

goto_modelt::goto_modelt ( goto_modelt &&  other)
inline

Definition at line 60 of file goto_model.h.

Member Function Documentation

◆ can_produce_function()

bool goto_modelt::can_produce_function ( const irep_idt id) const
inlineoverridevirtual

Determines if this model can produce a body for the given function.

Parameters
idfunction ID to query
Returns
true if we can produce a function body, or false if we would leave it a bodyless stub.

Implements abstract_goto_modelt.

Definition at line 93 of file goto_model.h.

References goto_functionst::function_map, and goto_functions.

◆ clear()

void goto_modelt::clear ( void  )
inline

◆ get_goto_function()

const goto_functionst::goto_functiont& goto_modelt::get_goto_function ( const irep_idt id)
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.

Parameters
idfunction to get
Returns
function body

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().

◆ get_goto_functions()

const goto_functionst& goto_modelt::get_goto_functions ( ) const
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.

◆ get_symbol_table()

const symbol_tablet& goto_modelt::get_symbol_table ( ) const
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.

◆ operator=() [1/2]

goto_modelt& goto_modelt::operator= ( const goto_modelt )
delete

◆ operator=() [2/2]

goto_modelt& goto_modelt::operator= ( goto_modelt &&  other)
inline

Definition at line 66 of file goto_model.h.

References goto_functions, and symbol_table.

◆ output()

void goto_modelt::output ( std::ostream &  out) const
inline

Definition at line 40 of file goto_model.h.

References goto_functions, goto_functionst::output(), and symbol_table.

◆ unload()

void goto_modelt::unload ( const irep_idt name)
inline

Definition at line 73 of file goto_model.h.

References goto_functions, and goto_functionst::unload().

Member Data Documentation

◆ goto_functions

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_table

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().


The documentation for this class was generated from the following file: