Container for an instruction of the goto-program. More...

#include <goto_program.h>

Classes
struct	loop_contract_datat

Public Types
typedef std::list< classinstructiont >::iterator	targett
	the targets for gotos and catch
typedef std::list< classinstructiont >::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

Public Member Functions
loop_contract_datat &	loop_contract_payload ()
targett	get_target () const
	Returns the first (and only) successor for the usual case of a single target.
void	set_target (targett t)
	Sets the first (and only) successor for the usual case of a single target.
bool	has_target () const
bool	is_target () const
	is this node a branch target?
void	clear (goto_program_instruction_typet _type)
	clear the node
void	make_goto ()
void	make_location (const locationt &l)
void	make_return ()
void	make_function_call (const expr2tc &_code)
void	make_skip ()
void	make_throw ()
void	make_catch ()
void	make_assertion (const expr2tc &g)
void	make_assumption (const expr2tc &g)
void	make_assignment ()
void	make_other ()
void	make_decl ()
void	make_dead ()
void	make_atomic_begin ()
void	make_atomic_end ()
void	make_goto (targett _target)
void	make_goto (targett _target, const expr2tc &g)
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_assume () const
bool	is_assert () const
bool	is_loop_invariant () const
bool	is_atomic_begin () const
bool	is_atomic_end () const
bool	is_end_function () const
	instructiont ()
	instructiont (goto_program_instruction_typet _type)
	instructiont (const instructiont &other)
instructiont &	operator= (const instructiont &other)
	instructiont (instructiont &&other)
instructiont &	operator= (instructiont &&other)
void	swap (instructiont &instruction)
	swap two instructions
void	add_loop_invariant (const expr2tc &invariant)
std::list< expr2tc >	get_loop_invariants () const
void	add_loop_assigns_target (const expr2tc &target)
std::list< expr2tc >	get_loop_assigns_targets () const
bool	is_backwards_goto () const
	Returns true if the instruction is a backwards branch.
bool	operator< (const class instructiont i1) const
void	dump () const
void	output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, bool show_location=true) const

Public Attributes
expr2tc	code
irep_idt	function
	function this belongs to
locationt	location
	the location of the instruction in the source file
goto_program_instruction_typet	type
	what kind of instruction?
expr2tc	guard
	guard for gotos, assume, assert
std::unique_ptr< loop_contract_datat >	loop_contract_data
targetst	targets
labelst	labels
bool	inductive_step_instruction
bool	inductive_assertion
bool	flipped_guard
bool	loop_invariant_havoc
std::vector< std::string >	switch_case_ids
unsigned	location_number
unsigned	loop_number
	Number unique per function to identify loops.
unsigned	pragma_unroll_count
	Pragma-specified unroll count (0 = not specified, UINT_MAX = unlimited).
unsigned	target_number
unsigned int	scope_id = 0
unsigned int	parent_scope_id = 0
	Id of the parent scope for the current "scope_id".

Detailed Description

Container for an instruction of the goto-program.

Member Typedef Documentation

◆ const_targetst

typedef std::list<const_targett> goto_programt::instructiont::const_targetst

◆ const_targett

typedef std::list<classinstructiont>::const_iterator goto_programt::instructiont::const_targett

◆ labelst

typedef std::list<irep_idt> goto_programt::instructiont::labelst

goto target labels

◆ targetst

typedef std::list<targett> goto_programt::instructiont::targetst

◆ targett

typedef std::list<classinstructiont>::iterator goto_programt::instructiont::targett

the targets for gotos and catch

Constructor & Destructor Documentation

◆ instructiont() [1/4]

goto_programt::instructiont::instructiont ( )

inline

◆ instructiont() [2/4]

goto_programt::instructiont::instructiont ( goto_program_instruction_typet _type )

inline

◆ instructiont() [3/4]

goto_programt::instructiont::instructiont ( const instructiont & other )

inline

◆ instructiont() [4/4]

goto_programt::instructiont::instructiont ( instructiont && other )

inline

Member Function Documentation

◆ add_loop_assigns_target()

void goto_programt::instructiont::add_loop_assigns_target ( const expr2tc & target )

inline

◆ add_loop_invariant()

void goto_programt::instructiont::add_loop_invariant ( const expr2tc & invariant )

inline

◆ clear()

void goto_programt::instructiont::clear ( goto_program_instruction_typet _type )

inline

clear the node

◆ dump()

void goto_programt::instructiont::dump ( ) const

◆ get_loop_assigns_targets()

std::list< expr2tc > goto_programt::instructiont::get_loop_assigns_targets ( ) const

inline

◆ get_loop_invariants()

std::list< expr2tc > goto_programt::instructiont::get_loop_invariants ( ) const

inline

◆ get_target()

targett goto_programt::instructiont::get_target ( ) const

inline

Returns the first (and only) successor for the usual case of a single target.

◆ has_target()

bool goto_programt::instructiont::has_target ( ) const

inline

◆ is_assert()

bool goto_programt::instructiont::is_assert ( ) const

inline

◆ is_assign()

bool goto_programt::instructiont::is_assign ( ) const

inline

◆ is_assume()

bool goto_programt::instructiont::is_assume ( ) const

inline

◆ is_atomic_begin()

bool goto_programt::instructiont::is_atomic_begin ( ) const

inline

◆ is_atomic_end()

bool goto_programt::instructiont::is_atomic_end ( ) const

inline

◆ is_backwards_goto()

bool goto_programt::instructiont::is_backwards_goto ( ) const

inline

Returns true if the instruction is a backwards branch.

◆ is_catch()

bool goto_programt::instructiont::is_catch ( ) const

inline

◆ is_decl()

bool goto_programt::instructiont::is_decl ( ) const

inline

◆ is_end_function()

bool goto_programt::instructiont::is_end_function ( ) const

inline

◆ is_function_call()

bool goto_programt::instructiont::is_function_call ( ) const

inline

◆ is_goto()

bool goto_programt::instructiont::is_goto ( ) const

inline

◆ is_location()

bool goto_programt::instructiont::is_location ( ) const

inline

◆ is_loop_invariant()

bool goto_programt::instructiont::is_loop_invariant ( ) const

inline

◆ is_other()

bool goto_programt::instructiont::is_other ( ) const

inline

◆ is_return()

bool goto_programt::instructiont::is_return ( ) const

inline

◆ is_skip()

bool goto_programt::instructiont::is_skip ( ) const

inline

◆ is_target()

bool goto_programt::instructiont::is_target ( ) const

inline

is this node a branch target?

◆ is_throw()

bool goto_programt::instructiont::is_throw ( ) const

inline

◆ loop_contract_payload()

loop_contract_datat & goto_programt::instructiont::loop_contract_payload ( )

inline

◆ make_assertion()

void goto_programt::instructiont::make_assertion ( const expr2tc & g )

inline

◆ make_assignment()

void goto_programt::instructiont::make_assignment ( )

inline

◆ make_assumption()

void goto_programt::instructiont::make_assumption ( const expr2tc & g )

inline

◆ make_atomic_begin()

void goto_programt::instructiont::make_atomic_begin ( )

inline

◆ make_atomic_end()

void goto_programt::instructiont::make_atomic_end ( )

inline

◆ make_catch()

void goto_programt::instructiont::make_catch ( )

inline

◆ make_dead()

void goto_programt::instructiont::make_dead ( )

inline

◆ make_decl()

void goto_programt::instructiont::make_decl ( )

inline

◆ make_function_call()

void goto_programt::instructiont::make_function_call ( const expr2tc & _code )

inline

◆ make_goto() [1/3]

void goto_programt::instructiont::make_goto ( )

inline

◆ make_goto() [2/3]

void goto_programt::instructiont::make_goto ( targett _target )

inline

◆ make_goto() [3/3]

void goto_programt::instructiont::make_goto	(	targett	_target,
		const expr2tc &	g )

inline

◆ make_location()

void goto_programt::instructiont::make_location ( const locationt & l )

inline

◆ make_other()

void goto_programt::instructiont::make_other ( )

inline

◆ make_return()

void goto_programt::instructiont::make_return ( )

inline

◆ make_skip()

void goto_programt::instructiont::make_skip ( )

inline

◆ make_throw()

void goto_programt::instructiont::make_throw ( )

inline

◆ operator<()

bool goto_programt::instructiont::operator< ( const class instructiont i1 ) const

inline

◆ operator=() [1/2]

instructiont & goto_programt::instructiont::operator= ( const instructiont & other )

inline

◆ operator=() [2/2]

instructiont & goto_programt::instructiont::operator= ( instructiont && other )

inline

◆ output_instruction()

void goto_programt::instructiont::output_instruction	(	const class namespacet &	ns,
		const irep_idt &	identifier,
		std::ostream &	out,
		bool	show_location = true ) const

◆ set_target()

void goto_programt::instructiont::set_target ( targett t )

inline

Sets the first (and only) successor for the usual case of a single target.

◆ swap()

void goto_programt::instructiont::swap ( instructiont & instruction )

inline

swap two instructions

Member Data Documentation

◆ code

expr2tc goto_programt::instructiont::code

◆ flipped_guard

bool goto_programt::instructiont::flipped_guard

◆ function

irep_idt goto_programt::instructiont::function

function this belongs to

◆ guard

expr2tc goto_programt::instructiont::guard

guard for gotos, assume, assert

◆ inductive_assertion

bool goto_programt::instructiont::inductive_assertion

◆ inductive_step_instruction

bool goto_programt::instructiont::inductive_step_instruction

◆ labels

labelst goto_programt::instructiont::labels

◆ location

locationt goto_programt::instructiont::location

the location of the instruction in the source file

◆ location_number

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.

◆ loop_contract_data

std::unique_ptr<loop_contract_datat> goto_programt::instructiont::loop_contract_data

◆ loop_invariant_havoc

bool goto_programt::instructiont::loop_invariant_havoc

◆ loop_number

unsigned goto_programt::instructiont::loop_number

Number unique per function to identify loops.

◆ parent_scope_id

unsigned int goto_programt::instructiont::parent_scope_id = 0

Id of the parent scope for the current "scope_id".

◆ pragma_unroll_count

unsigned goto_programt::instructiont::pragma_unroll_count

Pragma-specified unroll count (0 = not specified, UINT_MAX = unlimited).

◆ scope_id

unsigned int goto_programt::instructiont::scope_id = 0

Id of the scope within which a variable is declared (i.e., DECL). It does not have a lot of meaning for other types of instructions.

◆ switch_case_ids

std::vector<std::string> goto_programt::instructiont::switch_case_ids

◆ target_number

unsigned goto_programt::instructiont::target_number

A number to identify branch targets. This is -1 if it's not a target.

◆ targets

targetst goto_programt::instructiont::targets

◆ type

goto_program_instruction_typet goto_programt::instructiont::type

what kind of instruction?

The documentation for this class was generated from the following files:

src/goto-programs/goto_program.h
src/goto-programs/goto_program.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ const_targetst

◆ const_targett

◆ labelst

◆ targetst

◆ targett

Constructor & Destructor Documentation

◆ instructiont() [1/4]

◆ instructiont() [2/4]

◆ instructiont() [3/4]

◆ instructiont() [4/4]

Member Function Documentation

◆ add_loop_assigns_target()

◆ add_loop_invariant()

◆ clear()

◆ dump()

◆ get_loop_assigns_targets()

◆ get_loop_invariants()

◆ get_target()

◆ has_target()

◆ is_assert()

◆ is_assign()

◆ is_assume()

◆ is_atomic_begin()

◆ is_atomic_end()

◆ is_backwards_goto()

◆ is_catch()

◆ is_decl()

◆ is_end_function()

◆ is_function_call()

◆ is_goto()

◆ is_location()

◆ is_loop_invariant()

◆ is_other()

◆ is_return()

◆ is_skip()

◆ is_target()

◆ is_throw()

◆ loop_contract_payload()

◆ make_assertion()

◆ make_assignment()

◆ make_assumption()

◆ make_atomic_begin()

◆ make_atomic_end()

◆ make_catch()

◆ make_dead()

◆ make_decl()

◆ make_function_call()

◆ make_goto() [1/3]

◆ make_goto() [2/3]

◆ make_goto() [3/3]

◆ make_location()

◆ make_other()

◆ make_return()

◆ make_skip()

◆ make_throw()

◆ operator<()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ output_instruction()

◆ set_target()

◆ swap()

Member Data Documentation

◆ code

◆ flipped_guard

◆ function

◆ guard

◆ inductive_assertion

◆ inductive_step_instruction

◆ labels

◆ location

◆ location_number

◆ loop_contract_data

◆ loop_invariant_havoc

◆ loop_number