cprover
|
Concrete Goto Program. More...
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, exprt > | const_target_hash |
Functions | |
bool | operator< (const goto_programt::const_targett i1, const goto_programt::const_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 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().
#define Forall_goto_program_instructions | ( | it, | |
program | |||
) |
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 struct const_target_hash_templatet< codet, exprt > const_target_hash |
Definition at line 86 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 260 of file goto_program.cpp.
References code_function_callt::arguments(), ASSERT, ASSIGN, ASSUME, forall_expr, FUNCTION_CALL, GOTO, 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(), and to_code_return().
Referenced by objects_read(), and uninitialized_domaint::transform().
std::list<exprt> expressions_written | ( | const goto_programt::instructiont & | ) |
Definition at line 305 of file goto_program.cpp.
References ASSIGN, FUNCTION_CALL, irept::is_not_nil(), code_assignt::lhs(), code_function_callt::lhs(), to_code_assign(), and to_code_function_call().
Referenced by objects_written(), and uninitialized_domaint::transform().
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().
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().
|
inline |
Definition at line 78 of file goto_program.h.