cprover
goto_program.h File Reference

Concrete Goto Program. More...

#include <set>
#include <util/std_code.h>
#include "goto_program_template.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 specialization of goto_program_templatet over goto programs in which instructions have codet type. More...
 

Macros

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

Typedefs

typedef struct const_target_hash_templatet< codet, exprtconst_target_hash
 

Functions

bool operator< (const goto_programt::const_targett i1, const goto_programt::const_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 68 of file goto_program.h.

Referenced by call_grapht::add(), uninitializedt::add_assertions(), remove_exceptionst::add_exceptional_returns(), invariant_propagationt::add_objects(), all_unreachable(), basic_blockst::basic_blockst(), localst::build(), locst::build(), dirtyt::build(), goto_program2codet::build_dead_map(), custom_bitvector_analysist::check(), goto_unwindt::unwind_logt::cleanup(), goto_inlinet::goto_inline_logt::cleanup(), concurrency_instrumentationt::collect(), goto_checkt::collect_allocations(), collect_eloc(), is_threadedt::compute(), fence_all_sharedt::compute(), fence_volatilet::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(), convert(), value_set_analysist::convert(), document_propertiest::doit(), goto_instrument_parse_optionst::doit(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), acceleration_utilst::find_modified(), find_used_functions(), 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(), path_searcht::initialize_property_map(), instrument_intervals(), instrumentert::is_cfg_spurious(), is_empty(), static_analyzert::json_report(), list_calls_and_arguments(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), goto_program2codet::operator()(), local_may_alias_factoryt::operator()(), local_bitvector_analysist::output(), local_may_aliast::output(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), static_analysis_baset::output(), ai_baset::output(), change_impactt::output_change_impact(), ai_baset::output_json(), ai_baset::output_xml(), static_analyzert::plain_text_report(), print_path_lengths(), goto_program2codet::scan_for_varargs(), show_call_sequences(), show_loop_ids(), show_loop_ids_json(), slice_global_inits(), static_analysis_baset::update(), write_goto_binary_v3(), and static_analyzert::xml_report().

◆ 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 73 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_convertt::convert_bp_enforce(), 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_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(), remove_instanceoft::lower_instanceof(), mmio(), model_argc_argv(), mutex_init_instrumentation(), nondet_static(), nondet_volatile(), full_slicert::operator()(), string_instrumentationt::operator()(), remove_asmt::process_function(), const_function_pointer_propagationt::propagate(), race_check(), remove_complex(), remove_function_pointerst::remove_function_pointer(), remove_function_pointerst::remove_function_pointers(), remove_skip(), remove_unreachable(), remove_vector(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), rename_symbols_in_function(), constant_propagator_ait::replace(), replace_async(), remove_returnst::replace_returns(), remove_returnst::restore_returns(), rewrite_union(), invariant_propagationt::simplify(), skip_loops(), reachability_slicert::slice(), slice_global_inits(), 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().

Typedef Documentation

◆ const_target_hash

Definition at line 86 of file goto_program.h.

Function Documentation

◆ as_string()

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

◆ expressions_read()

◆ expressions_written()

std::list<exprt> expressions_written ( const goto_programt::instructiont &  )

◆ objects_read()

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

Definition at line 357 of file goto_program.cpp.

References expressions_read(), forall_expr_list, and objects_read().

◆ objects_written()

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

Definition at line 384 of file goto_program.cpp.

References expressions_written(), forall_expr_list, and objects_written().

◆ operator<()

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

Definition at line 78 of file goto_program.h.