cprover
goto_program.h File Reference

Concrete Goto Program. More...

#include <iosfwd>
#include <set>
#include <limits>
#include <sstream>
#include <string>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <util/source_location.h>
#include <util/std_expr.h>
#include <util/std_code.h>
Include dependency graph for goto_program.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  goto_programt
 A generic container class for the GOTO intermediate representation of one function. More...
 
class  goto_programt::instructiont
 This class represents an instruction in the GOTO intermediate representation. More...
 
struct  const_target_hash
 
struct  pointee_address_equalt
 Functor to check whether iterators from different collections point at the same object. More...
 

Macros

#define forall_goto_program_instructions(it, program)
 
#define Forall_goto_program_instructions(it, program)
 

Enumerations

enum  goto_program_instruction_typet {
  NO_INSTRUCTION_TYPE = 0, GOTO = 1, ASSUME = 2, ASSERT = 3,
  OTHER = 4, SKIP = 5, START_THREAD = 6, END_THREAD = 7,
  LOCATION = 8, END_FUNCTION = 9, ATOMIC_BEGIN = 10, ATOMIC_END = 11,
  RETURN = 12, ASSIGN = 13, DECL = 14, DEAD = 15,
  FUNCTION_CALL = 16, THROW = 17, CATCH = 18, INCOMPLETE_GOTO = 19
}
 The type of an instruction in a GOTO program. More...
 

Functions

std::ostream & operator<< (std::ostream &, goto_program_instruction_typet)
 
bool order_const_target (const goto_programt::const_targett i1, const goto_programt::const_targett i2)
 
bool operator< (const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
 
bool operator< (const goto_programt::targett &i1, const goto_programt::targett &i2)
 
std::list< exprtobjects_read (const goto_programt::instructiont &)
 
std::list< exprtobjects_written (const goto_programt::instructiont &)
 
std::list< exprtexpressions_read (const goto_programt::instructiont &)
 
std::list< exprtexpressions_written (const goto_programt::instructiont &)
 
std::string as_string (const namespacet &ns, const goto_programt::instructiont &)
 

Detailed Description

Concrete Goto Program.

Definition in file goto_program.h.

Macro Definition Documentation

◆ forall_goto_program_instructions

#define forall_goto_program_instructions (   it,
  program 
)
Value:
for(goto_programt::instructionst::const_iterator \
it=(program).instructions.begin(); \
it!=(program).instructions.end(); it++)

Definition at line 735 of file goto_program.h.

Referenced by uninitializedt::add_assertions(), invariant_propagationt::add_objects(), all_unreachable(), localst::build(), dirtyt::build(), goto_program2codet::build_dead_map(), build_dead_map_from_ai(), custom_bitvector_analysist::check(), goto_unwindt::unwind_logt::cleanup(), goto_inlinet::goto_inline_logt::cleanup(), concurrency_instrumentationt::collect(), goto_checkt::collect_allocations(), collect_eloc(), uncaught_exceptions_analysist::collect_uncaught_exceptions(), is_threadedt::compute(), compute_address_taken_functions(), compute_called_functions(), goto_program_coverage_recordt::compute_coverage_lines(), rw_set_functiont::compute_rec(), static_analysis_baset::concurrent_fixedpoint(), ai_baset::concurrent_fixedpoint(), cover_basic_blocks_javat::cover_basic_blocks_javat(), cover_basic_blockst::cover_basic_blockst(), document_propertiest::doit(), goto_instrument_parse_optionst::doit(), acceleration_utilst::find_modified(), find_used_functions(), forall_callsites(), remove_exceptionst::function_or_callees_may_throw(), static_analysis_baset::generate_states(), goto_programt::get_decl_identifiers(), function_modifiest::get_modifies_function(), goto_rw(), goto_convert_functionst::hide(), invariant_propagationt::initialize(), ai_baset::initialize(), property_checkert::initialize_property_map(), instrument_intervals(), instrumentert::is_cfg_spurious(), is_empty(), list_calls_and_arguments(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), goto_program2codet::operator()(), local_may_alias_factoryt::operator()(), trivial_functions_filtert::operator()(), local_bitvector_analysist::output(), local_may_aliast::output(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), local_safe_pointerst::output(), static_analysis_baset::output(), ai_baset::output(), change_impactt::output_change_impact(), ai_baset::output_json(), local_safe_pointerst::output_safe_dereferences(), ai_baset::output_xml(), print_path_lengths(), cover_basic_blockst::report_block_anomalies(), goto_program2codet::scan_for_varargs(), show_loop_ids(), show_loop_ids_json(), slice_global_inits(), static_verifier(), static_analysis_baset::update(), value_sets_to_xml(), and write_goto_binary_v3().

◆ Forall_goto_program_instructions

#define Forall_goto_program_instructions (   it,
  program 
)
Value:
for(goto_programt::instructionst::iterator \
it=(program).instructions.begin(); \
it!=(program).instructions.end(); it++)

Definition at line 740 of file goto_program.h.

Referenced by string_abstractiont::abstract(), uninitializedt::add_assertions(), overflow_instrumentert::add_overflow_checks(), adjust_float_expressions(), shared_bufferst::affected_by_delay(), branch(), trace_automatont::build_alphabet(), sat_path_enumeratort::build_fixed(), disjunctive_polynomial_accelerationt::build_fixed(), code_contractst::code_contracts(), goto_convert_functionst::convert_function(), string_abstractiont::declare_define_locals(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), finish_catch_push_targets(), function_exit(), goto_checkt::goto_check(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), goto_inlinet::insert_function_body(), escape_analysist::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_exceptions(), instrument_intervals(), interrupt(), introduce_temporaries(), instrumentert::is_cfg_spurious(), link_functions(), mmio(), model_argc_argv(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), replace_callst::operator()(), full_slicert::operator()(), cover_instrumenter_baset::operator()(), string_instrumentationt::operator()(), linker_script_merget::pointerize_linker_defined_symbols(), remove_asmt::process_function(), race_check(), remove_complex(), remove_function_pointerst::remove_function_pointer(), remove_function_pointerst::remove_function_pointers(), remove_unreachable(), remove_vector(), remove_virtual_functionst::remove_virtual_function(), rename_symbols_in_function(), constant_propagator_ait::replace(), remove_returnst::replace_returns(), remove_returnst::restore_returns(), rewrite_union(), invariant_propagationt::simplify(), skip_loops(), reachability_slicert::slice(), slice_global_inits(), static_simplifier(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), goto_unwindt::unwind(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().

Enumeration Type Documentation

◆ goto_program_instruction_typet

The type of an instruction in a GOTO program.

Enumerator
NO_INSTRUCTION_TYPE 
GOTO 
ASSUME 
ASSERT 
OTHER 
SKIP 
START_THREAD 
END_THREAD 
LOCATION 
END_FUNCTION 
ATOMIC_BEGIN 
ATOMIC_END 
RETURN 
ASSIGN 
DECL 
DEAD 
FUNCTION_CALL 
THROW 
CATCH 
INCOMPLETE_GOTO 

Definition at line 29 of file goto_program.h.

Function Documentation

◆ as_string()

std::string as_string ( const namespacet ns,
const goto_programt::instructiont  
)

◆ expressions_read()

◆ expressions_written()

◆ objects_read()

std::list<exprt> objects_read ( const goto_programt::instructiont )

Definition at line 358 of file goto_program.cpp.

References expressions_read(), and objects_read().

◆ objects_written()

std::list<exprt> objects_written ( const goto_programt::instructiont )

Definition at line 385 of file goto_program.cpp.

References expressions_written(), and objects_written().

◆ operator<() [1/2]

bool operator< ( const goto_programt::const_targett i1,
const goto_programt::const_targett i2 
)
inline

Definition at line 745 of file goto_program.h.

References order_const_target().

◆ operator<() [2/2]

bool operator< ( const goto_programt::targett i1,
const goto_programt::targett i2 
)
inline

Definition at line 752 of file goto_program.h.

◆ operator<<()

std::ostream& operator<< ( std::ostream &  ,
goto_program_instruction_typet   
)

◆ order_const_target()

bool order_const_target ( const goto_programt::const_targett  i1,
const goto_programt::const_targett  i2 
)
inline

Definition at line 704 of file goto_program.h.

Referenced by operator<().