cprover
|
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>
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< exprt > | objects_read (const goto_programt::instructiont &) |
std::list< exprt > | objects_written (const goto_programt::instructiont &) |
std::list< exprt > | expressions_read (const goto_programt::instructiont &) |
std::list< exprt > | expressions_written (const goto_programt::instructiont &) |
std::string | as_string (const namespacet &ns, const goto_programt::instructiont &) |
Concrete Goto Program.
Definition in file goto_program.h.
#define forall_goto_program_instructions | ( | it, | |
program | |||
) |
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().
#define Forall_goto_program_instructions | ( | it, | |
program | |||
) |
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().
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.
std::string as_string | ( | const namespacet & | ns, |
const goto_programt::instructiont & | |||
) |
std::list<exprt> expressions_read | ( | const goto_programt::instructiont & | ) |
Definition at line 261 of file goto_program.cpp.
References code_function_callt::arguments(), ASSERT, ASSIGN, ASSUME, goto_programt::instructiont::code, forall_expr, FUNCTION_CALL, GOTO, goto_programt::instructiont::guard, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), parse_lhs_read(), RETURN, code_returnt::return_value(), code_assignt::rhs(), to_code_assign(), to_code_function_call(), to_code_return(), and goto_programt::instructiont::type.
Referenced by objects_read(), and uninitialized_domaint::transform().
std::list<exprt> expressions_written | ( | const goto_programt::instructiont & | ) |
Definition at line 306 of file goto_program.cpp.
References ASSIGN, goto_programt::instructiont::code, FUNCTION_CALL, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), to_code_assign(), to_code_function_call(), and goto_programt::instructiont::type.
Referenced by objects_written(), and uninitialized_domaint::transform().
std::list<exprt> objects_read | ( | const goto_programt::instructiont & | ) |
Definition at line 358 of file goto_program.cpp.
References expressions_read(), and objects_read().
std::list<exprt> objects_written | ( | const goto_programt::instructiont & | ) |
Definition at line 385 of file goto_program.cpp.
References expressions_written(), and objects_written().
|
inline |
Definition at line 745 of file goto_program.h.
References order_const_target().
|
inline |
Definition at line 752 of file goto_program.h.
std::ostream& operator<< | ( | std::ostream & | , |
goto_program_instruction_typet | |||
) |
Definition at line 16 of file goto_program_template.cpp.
References ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, DEAD, DECL, END_FUNCTION, END_THREAD, FUNCTION_CALL, GOTO, LOCATION, NO_INSTRUCTION_TYPE, OTHER, RETURN, SKIP, and START_THREAD.
|
inline |
Definition at line 704 of file goto_program.h.
Referenced by operator<().