cprover
|
This class represents an instruction in the GOTO intermediate representation. More...
#include <goto_program.h>
Public Types | |
typedef std::list< instructiont >::iterator | targett |
The target for gotos and for start_thread nodes. More... | |
typedef std::list< instructiont >::const_iterator | const_targett |
typedef std::list< targett > | targetst |
typedef std::list< const_targett > | const_targetst |
typedef std::list< irep_idt > | labelst |
Goto target labels. More... | |
Public Member Functions | |
targett | get_target () const |
Returns the first (and only) successor for the usual case of a single target. More... | |
void | set_target (targett t) |
Sets the first (and only) successor for the usual case of a single target. More... | |
bool | has_target () const |
bool | is_target () const |
Is this node a branch target? More... | |
void | clear (goto_program_instruction_typet _type) |
Clear the node. More... | |
void | make_return () |
void | make_skip () |
void | make_location (const source_locationt &l) |
void | make_throw () |
void | make_catch () |
void | make_assertion (const exprt &g) |
void | make_assumption (const exprt &g) |
void | make_assignment () |
void | make_other (const codet &_code) |
void | make_decl () |
void | make_dead () |
void | make_atomic_begin () |
void | make_atomic_end () |
void | make_end_function () |
void | make_incomplete_goto (const code_gotot &_code) |
void | make_goto (targett _target) |
void | make_goto (targett _target, const exprt &g) |
void | complete_goto (targett _target) |
void | make_assignment (const codet &_code) |
void | make_decl (const codet &_code) |
void | make_function_call (const codet &_code) |
bool | is_goto () const |
bool | is_return () const |
bool | is_assign () const |
bool | is_function_call () const |
bool | is_throw () const |
bool | is_catch () const |
bool | is_skip () const |
bool | is_location () const |
bool | is_other () const |
bool | is_decl () const |
bool | is_dead () const |
bool | is_assume () const |
bool | is_assert () const |
bool | is_atomic_begin () const |
bool | is_atomic_end () const |
bool | is_start_thread () const |
bool | is_end_thread () const |
bool | is_end_function () const |
bool | is_incomplete_goto () const |
instructiont () | |
instructiont (goto_program_instruction_typet _type) | |
void | swap (instructiont &instruction) |
Swap two instructions. More... | |
bool | is_backwards_goto () const |
Returns true if the instruction is a backwards branch. More... | |
std::string | to_string () const |
Public Attributes | |
codet | code |
irep_idt | function |
The function this instruction belongs to. More... | |
source_locationt | source_location |
The location of the instruction in the source file. More... | |
goto_program_instruction_typet | type |
What kind of instruction? More... | |
exprt | guard |
Guard for gotos, assume, assert. More... | |
targetst | targets |
The list of successor instructions. More... | |
labelst | labels |
std::set< targett > | incoming_edges |
unsigned | location_number |
A globally unique number to identify a program location. More... | |
unsigned | loop_number |
Number unique per function to identify loops. More... | |
unsigned | target_number |
A number to identify branch targets. More... | |
Static Public Attributes | |
static const unsigned | nil_target |
Uniquely identify an invalid target or location. More... | |
This class represents an instruction in the GOTO intermediate representation.
Three fields are key:
The meaning of an instruction node depends on the type
field. Different kinds of instructions make use of the fields guard
and code
for different purposes. We list below, using a mixture of pseudo code and plain English, the meaning of different kinds of instructions. We use guard
, code
, and targets
to mean the value of the respective fields in this class:
targets
if and only if guard
is true. More than one target is deprecated. Its semantics was a non-deterministic choice.code
(which shall be either nil or an instance of code_returnt) and then jump to the end of the function. Many analysis tools remove these instructions before they start.code
(an instance of code_declt), the life-time of which is bounded by a corresponding DEAD instruction. Non-static symbols must be DECL'd before they are used.code
. After a DEAD instruction the symbol must be DECL'd again before use.code
(an instance of code_function_callt).code
(an instance of code_assignt) to the value of the right-hand side.code
(an instance of codet of kind ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input, ID_output, ...).guard
to evaluate to true. Assume does not "retro-actively" affect the thread or any ASSERTs.guard
is true in all possible executions, otherwise it is false / unsafe. The status of the assertion does not affect execution in any way.exception1
, ..., exceptionN
where the list of exceptions is extracted from the code
field Many analysis tools remove these instructions before they start.exception1
is thrown, then goto target1
,exceptionN
is thrown, then goto targetN
. The list of exceptions is obtained from the code
field and the list of targets from the targets
field.Definition at line 173 of file goto_program.h.
typedef std::list<const_targett> goto_programt::instructiont::const_targetst |
Definition at line 195 of file goto_program.h.
typedef std::list<instructiont>::const_iterator goto_programt::instructiont::const_targett |
Definition at line 193 of file goto_program.h.
typedef std::list<irep_idt> goto_programt::instructiont::labelst |
Goto target labels.
Definition at line 222 of file goto_program.h.
typedef std::list<targett> goto_programt::instructiont::targetst |
Definition at line 194 of file goto_program.h.
typedef std::list<instructiont>::iterator goto_programt::instructiont::targett |
The target for gotos and for start_thread nodes.
Definition at line 192 of file goto_program.h.
|
inline |
Definition at line 323 of file goto_program.h.
|
inlineexplicit |
Definition at line 328 of file goto_program.h.
|
inline |
Clear the node.
Definition at line 233 of file goto_program.h.
References code, guard, irept::make_nil(), targets, and type.
Referenced by make_assertion(), make_assignment(), make_assumption(), make_atomic_begin(), make_atomic_end(), make_catch(), make_dead(), make_decl(), make_end_function(), make_function_call(), make_goto(), make_incomplete_goto(), make_location(), make_other(), make_return(), make_skip(), make_throw(), and instrumentert::cfg_visitort::visit_cfg_propagate().
|
inline |
Definition at line 275 of file goto_program.h.
References GOTO, INCOMPLETE_GOTO, PRECONDITION, targets, and type.
Referenced by goto_convertt::finish_gotos().
|
inline |
Returns the first (and only) successor for the usual case of a single target.
Definition at line 202 of file goto_program.h.
References PRECONDITION, and targets.
Referenced by cfg_baset< cfg_nodet >::compute_edges_goto(), concurrent_cfg_baset< T, P, I >::compute_edges_start_thread(), unified_difft::instructions_equal(), goto_programt::output_instruction(), goto_symext::symex_goto(), and goto_symext::symex_start_thread().
|
inline |
Definition at line 216 of file goto_program.h.
References targets.
|
inline |
Definition at line 312 of file goto_program.h.
Referenced by goto_checkt::goto_check(), introduce_temporaries(), nondet_volatile(), and instrumentert::cfg_visitort::visit_cfg_assign().
|
inline |
Definition at line 302 of file goto_program.h.
Referenced by cone_of_influencet::cone_of_influence(), goto_program_dereferencet::dereference_instruction(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), is_assignment_from(), mmio(), nondet_static(), nondet_volatile(), does_remove_constt::operator()(), race_check(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 311 of file goto_program.h.
Referenced by as_string(), goto_programt::get_successors(), goto_checkt::goto_check(), introduce_temporaries(), nondet_volatile(), and goto_programt::output_instruction().
|
inline |
Definition at line 313 of file goto_program.h.
References ATOMIC_BEGIN, and type.
Referenced by instrumentert::cfg_visitort::visit_cfg_function().
|
inline |
Definition at line 314 of file goto_program.h.
References ATOMIC_END, and type.
Referenced by instrumentert::cfg_visitort::visit_cfg_function().
|
inline |
Returns true if the instruction is a backwards branch.
Definition at line 374 of file goto_program.h.
References is_goto(), location_number, and targets.
Referenced by goto_symext::symex_goto(), instrumentert::cfg_visitort::visit_cfg_goto(), and dott::write_edge().
|
inline |
Definition at line 305 of file goto_program.h.
|
inline |
Definition at line 310 of file goto_program.h.
Referenced by goto_checkt::goto_check().
|
inline |
Definition at line 309 of file goto_program.h.
Referenced by uninitializedt::add_assertions().
|
inline |
Definition at line 317 of file goto_program.h.
References END_FUNCTION, and type.
Referenced by goto_checkt::goto_check(), and goto_inlinet::insert_function_body().
|
inline |
Definition at line 316 of file goto_program.h.
References END_THREAD, and type.
Referenced by goto_programt::get_successors(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 303 of file goto_program.h.
References FUNCTION_CALL, and type.
Referenced by goto_checkt::collect_allocations(), goto_program_dereferencet::dereference_instruction(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), introduce_temporaries(), is_fence(), is_lwfence(), nondet_static(), nondet_volatile(), undefined_function_abort_path(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 300 of file goto_program.h.
Referenced by goto_programt::get_successors(), havoc_loopst::havoc_loop(), introduce_temporaries(), is_backwards_goto(), nondet_volatile(), and instrumentert::cfg_visitort::visit_cfg_function().
|
inline |
Definition at line 318 of file goto_program.h.
References INCOMPLETE_GOTO, and type.
|
inline |
Definition at line 307 of file goto_program.h.
|
inline |
Definition at line 308 of file goto_program.h.
Referenced by goto_program_dereferencet::dereference_instruction(), goto_checkt::goto_check(), is_fence(), is_lwfence(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 301 of file goto_program.h.
Referenced by goto_program_dereferencet::dereference_instruction(), goto_checkt::goto_check(), goto_symext::return_assignment(), and instrumentert::cfg_visitort::visit_cfg_function().
|
inline |
Definition at line 306 of file goto_program.h.
|
inline |
Definition at line 315 of file goto_program.h.
References START_THREAD, and type.
Referenced by goto_convertt::finish_gotos(), goto_programt::get_successors(), instrumentert::cfg_visitort::visit_cfg_function(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Is this node a branch target?
Definition at line 229 of file goto_program.h.
References nil_target, and target_number.
Referenced by goto_checkt::goto_check(), goto_programt::output_instruction(), and read_bin_goto_object_v3().
|
inline |
Definition at line 304 of file goto_program.h.
Referenced by goto_programt::get_successors(), and goto_checkt::goto_check().
|
inline |
Definition at line 247 of file goto_program.h.
|
inline |
Definition at line 249 of file goto_program.h.
References ASSIGN, and clear().
Referenced by string_abstractiont::abstract_pointer_assign(), introduce_temporaries(), linker_script_merget::ls_data2instructions(), and stack_depth().
|
inline |
Definition at line 282 of file goto_program.h.
|
inline |
Definition at line 248 of file goto_program.h.
References ASSUME, clear(), and guard.
Referenced by undefined_function_abort_path().
|
inline |
Definition at line 253 of file goto_program.h.
References ATOMIC_BEGIN, and clear().
Referenced by goto_convert_functionst::convert_function(), mmio(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 254 of file goto_program.h.
References ATOMIC_END, and clear().
|
inline |
Definition at line 246 of file goto_program.h.
|
inline |
Definition at line 252 of file goto_program.h.
|
inline |
Definition at line 251 of file goto_program.h.
|
inline |
Definition at line 288 of file goto_program.h.
|
inline |
Definition at line 255 of file goto_program.h.
References clear(), and END_FUNCTION.
|
inline |
Definition at line 294 of file goto_program.h.
References clear(), code, and FUNCTION_CALL.
Referenced by function_exit().
|
inline |
Definition at line 263 of file goto_program.h.
References clear(), GOTO, and targets.
Referenced by make_goto().
Definition at line 269 of file goto_program.h.
References guard, and make_goto().
|
inline |
Definition at line 257 of file goto_program.h.
References clear(), code, and INCOMPLETE_GOTO.
|
inline |
Definition at line 243 of file goto_program.h.
References clear(), LOCATION, and source_location.
|
inline |
Definition at line 250 of file goto_program.h.
|
inline |
Definition at line 241 of file goto_program.h.
|
inline |
Definition at line 242 of file goto_program.h.
Referenced by check_and_replace_target(), goto_checkt::goto_check(), and race_check().
|
inline |
Definition at line 245 of file goto_program.h.
|
inline |
Sets the first (and only) successor for the usual case of a single target.
Definition at line 210 of file goto_program.h.
References targets.
|
inline |
Swap two instructions.
Definition at line 339 of file goto_program.h.
References code, function, guard, source_location, targets, and type.
Referenced by overflow_instrumentert::accumulate_overflow(), interrupt(), acceleratet::make_overflow_loc(), mmio(), race_check(), and shared_bufferst::cfg_visitort::weak_memory().
|
inline |
Definition at line 386 of file goto_program.h.
References type.
Referenced by show_goto_functions_jsont::convert(), and show_goto_functions_xmlt::convert().
codet goto_programt::instructiont::code |
Definition at line 176 of file goto_program.h.
Referenced by string_abstractiont::abstract_pointer_assign(), overflow_instrumentert::accumulate_overflow(), uninitializedt::add_assertions(), acceleratet::add_dirty_checks(), as_string(), local_may_aliast::build(), local_bitvector_analysist::build(), clear(), goto_checkt::collect_allocations(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), cone_of_influencet::cone_of_influence(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), goto_program_dereferencet::dereference_instruction(), expressions_read(), expressions_written(), goto_convertt::finish_computed_gotos(), goto_convertt::finish_gotos(), get_modifies(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), goto_checkt::goto_check(), unified_difft::instructions_equal(), taint_analysist::instrument(), escape_analysist::instrument(), introduce_temporaries(), is_assignment_from(), is_fence(), is_lwfence(), make_assignment(), make_decl(), make_function_call(), make_incomplete_goto(), make_other(), mmio(), nondet_static(), nondet_volatile(), does_remove_constt::operator()(), goto_programt::output_instruction(), remove_asmt::process_instruction(), read_bin_goto_object_v3(), goto_symext::return_assignment(), swap(), goto_symext::symex_catch(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_goto(), goto_symext::symex_other(), goto_symext::symex_throw(), uncaught_exceptions_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), global_may_alias_domaint::transform(), interval_domaint::transform(), undefined_function_abort_path(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_function(), instrumentert::cfg_visitort::visit_cfg_function_call(), shared_bufferst::cfg_visitort::weak_memory(), shared_bufferst::write(), and write_goto_binary_v3().
irep_idt goto_programt::instructiont::function |
The function this instruction belongs to.
Definition at line 179 of file goto_program.h.
Referenced by string_abstractiont::abstract_pointer_assign(), code_contractst::apply_contract(), as_string(), check_apply_invariants(), function_exit(), goto_checkt::goto_check(), unified_difft::instructions_equal(), interrupt(), introduce_temporaries(), goto_programt::loop_id(), nondet_static(), read_bin_goto_object_v3(), swap(), shared_bufferst::cfg_visitort::weak_memory(), and write_goto_binary_v3().
exprt goto_programt::instructiont::guard |
Guard for gotos, assume, assert.
Definition at line 188 of file goto_program.h.
Referenced by uninitializedt::add_assertions(), acceleratet::add_dirty_checks(), code_contractst::apply_contract(), as_string(), local_cfgt::build(), check_apply_invariants(), clear(), cfg_baset< cfg_nodet >::compute_edges(), cfg_baset< cfg_nodet >::compute_edges_goto(), show_goto_functions_jsont::convert(), goto_program2codet::convert_goto_switch(), goto_program_dereferencet::dereference_instruction(), expressions_read(), goto_programt::get_successors(), goto_checkt::goto_check(), unified_difft::instructions_equal(), introduce_temporaries(), make_assertion(), make_assumption(), make_goto(), acceleratet::make_overflow_loc(), nondet_volatile(), goto_programt::output_instruction(), k_inductiont::process_loop(), read_bin_goto_object_v3(), swap(), goto_symext::symex_goto(), goto_symext::symex_step_goto(), custom_bitvector_domaint::transform(), interval_domaint::transform(), and write_goto_binary_v3().
std::set<targett> goto_programt::instructiont::incoming_edges |
Definition at line 226 of file goto_program.h.
Referenced by goto_symext::symex_goto(), goto_symext::symex_transition(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), instrumentert::cfg_visitort::visit_cfg_function_call(), instrumentert::cfg_visitort::visit_cfg_lwfence(), and instrumentert::cfg_visitort::visit_cfg_propagate().
labelst goto_programt::instructiont::labels |
Definition at line 223 of file goto_program.h.
Referenced by goto_checkt::goto_check(), goto_programt::output_instruction(), read_bin_goto_object_v3(), instrumentert::cfg_visitort::visit_cfg_assign(), and write_goto_binary_v3().
unsigned goto_programt::instructiont::location_number |
A globally unique number to identify a program location.
It's guaranteed to be ordered in program order within one goto_program.
Definition at line 364 of file goto_program.h.
Referenced by is_backwards_goto(), goto_programt::output_instruction(), and dott::write_edge().
unsigned goto_programt::instructiont::loop_number |
Number unique per function to identify loops.
Definition at line 367 of file goto_program.h.
Referenced by goto_programt::loop_id().
|
static |
Uniquely identify an invalid target or location.
Definition at line 357 of file goto_program.h.
Referenced by goto_programt::compute_target_numbers(), is_target(), and goto_convertt::optimize_guarded_gotos().
source_locationt goto_programt::instructiont::source_location |
The location of the instruction in the source file.
Definition at line 182 of file goto_program.h.
Referenced by string_abstractiont::abstract_pointer_assign(), uninitializedt::add_assertions(), code_contractst::apply_contract(), as_string(), check_apply_invariants(), goto_convert_functionst::convert_function(), goto_convertt::finish_computed_gotos(), bmc_all_propertiest::goalt::goalt(), goto_checkt::goto_check(), taint_analysist::instrument(), interrupt(), introduce_temporaries(), linker_script_merget::ls_data2instructions(), make_location(), nondet_static(), goto_programt::output_instruction(), race_check(), read_bin_goto_object_v3(), goto_symext::return_assignment(), swap(), undefined_function_abort_path(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), instrumentert::cfg_visitort::visit_cfg_assign(), instrumentert::cfg_visitort::visit_cfg_fence(), instrumentert::cfg_visitort::visit_cfg_lwfence(), shared_bufferst::cfg_visitort::weak_memory(), and write_goto_binary_v3().
unsigned goto_programt::instructiont::target_number |
A number to identify branch targets.
This is nil_target if it's not a target.
Definition at line 371 of file goto_program.h.
Referenced by is_target(), goto_programt::output_instruction(), read_bin_goto_object_v3(), and write_goto_binary_v3().
targetst goto_programt::instructiont::targets |
The list of successor instructions.
Definition at line 198 of file goto_program.h.
Referenced by as_string(), local_cfgt::build(), clear(), complete_goto(), cfg_baset< cfg_nodet >::compute_edges_catch(), goto_convertt::finish_gotos(), goto_programt::get_successors(), get_target(), has_target(), havoc_loopst::havoc_loop(), unified_difft::instructions_equal(), is_backwards_goto(), make_goto(), acceleratet::make_overflow_loc(), goto_programt::output_instruction(), set_target(), swap(), goto_symext::symex_catch(), goto_symext::symex_goto(), goto_symext::symex_start_thread(), uncaught_exceptions_domaint::transform(), and write_goto_binary_v3().
goto_program_instruction_typet goto_programt::instructiont::type |
What kind of instruction?
Definition at line 185 of file goto_program.h.
Referenced by uninitializedt::add_assertions(), as_string(), local_cfgt::build(), local_may_aliast::build(), local_bitvector_analysist::build(), clear(), complete_goto(), cfg_baset< cfg_nodet >::compute_edges(), expressions_read(), expressions_written(), goto_convertt::finish_computed_gotos(), goto_inlinet::insert_function_body(), unified_difft::instructions_equal(), taint_analysist::instrument(), escape_analysist::instrument(), is_assert(), is_assign(), is_assume(), is_atomic_begin(), is_atomic_end(), is_catch(), is_dead(), is_decl(), is_end_function(), is_end_thread(), is_function_call(), is_goto(), is_incomplete_goto(), is_location(), is_other(), is_return(), is_skip(), is_start_thread(), is_throw(), goto_programt::output_instruction(), read_bin_goto_object_v3(), swap(), to_string(), custom_bitvector_domaint::transform(), uncaught_exceptions_domaint::transform(), global_may_alias_domaint::transform(), escape_domaint::transform(), interval_domaint::transform(), points_tot::transform(), instrumentert::cfg_visitort::visit_cfg_function(), shared_bufferst::cfg_visitort::weak_memory(), and write_goto_binary_v3().