A specialization of goto_program_templatet over goto programs in which instructions have codet type. More...

#include <goto_program.h>

Inheritance diagram for goto_programt:

Collaboration diagram for goto_programt:

Public Types
typedef std::set< irep_idt >	decl_identifierst

Public Types inherited from goto_program_templatet< codet, exprt >
typedef std::list< instructiont >	instructionst

typedef instructionst::iterator	targett

typedef instructionst::const_iterator	const_targett

typedef std::list< targett >	targetst

typedef std::list< const_targett >	const_targetst

Public Member Functions
std::ostream &	output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
	See below. More...

std::ostream &	output_instruction (const class namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructiont &instruction) const

	goto_programt ()

	goto_programt (const goto_programt &)=delete

goto_programt &	operator= (const goto_programt &)=delete

	goto_programt (goto_programt &&other)

goto_programt &	operator= (goto_programt &&other)

void	get_decl_identifiers (decl_identifierst &decl_identifiers) const

Public Member Functions inherited from goto_program_templatet< codet, exprt >
	goto_program_templatet (const goto_program_templatet &)=delete
	Copying is deleted as this class contains pointers that cannot be copied. More...

	goto_program_templatet (goto_program_templatet &&other)

	goto_program_templatet ()
	Constructor. More...

goto_program_templatet &	operator= (const goto_program_templatet &)=delete

goto_program_templatet &	operator= (goto_program_templatet &&other)

targett	const_cast_target (const_targett t)
	Convert a const_targett to a targett - use with care and avoid whenever possible. More...

const_targett	const_cast_target (const_targett t) const
	Dummy for templates with possible const contexts. More...

std::list< Target >	get_successors (Target target) const

void	compute_incoming_edges ()

void	insert_before_swap (targett target)
	Insertion that preserves jumps to "target". More...

void	insert_before_swap (targett target, instructiont &instruction)
	Insertion that preserves jumps to "target". More...

void	insert_before_swap (targett target, goto_program_templatet< codet, exprt > &p)
	Insertion that preserves jumps to "target". More...

targett	insert_before (const_targett target)
	Insertion before the given target. More...

targett	insert_after (const_targett target)
	Insertion after the given target. More...

void	destructive_append (goto_program_templatet< codet, exprt > &p)
	Appends the given program, which is destroyed. More...

void	destructive_insert (const_targett target, goto_program_templatet< codet, exprt > &p)
	Inserts the given program at the given location. More...

targett	add_instruction ()
	Adds an instruction at the end. More...

targett	add_instruction (goto_program_instruction_typet type)
	Adds an instruction of given type at the end. More...

std::ostream &	output (const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
	Output goto program to given stream. More...

std::ostream &	output (std::ostream &out) const
	Output goto-program to given stream. More...

virtual std::ostream &	output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const=0
	Output a single instruction. More...

void	compute_target_numbers ()
	Compute the target numbers. More...

void	compute_location_numbers (unsigned &nr)
	Compute location numbers. More...

void	compute_location_numbers ()
	Compute location numbers. More...

void	compute_loop_numbers ()
	Compute loop numbers. More...

void	update ()
	Update all indices. More...

bool	empty () const
	Is the program empty? More...

virtual	~goto_program_templatet ()

void	swap (goto_program_templatet< codet, exprt > &program)
	Swap the goto program. More...

void	clear ()
	Clear the goto program. More...

targett	get_end_function ()

void	copy_from (const goto_program_templatet< codet, exprt > &src)
	Copy a full goto program, preserving targets. More...

bool	has_assertion () const
	Does the goto program have an assertion? More...

Additional Inherited Members
Static Public Member Functions inherited from goto_program_templatet< codet, exprt >
static const irep_idt	get_function_id (const_targett l)

static const irep_idt	get_function_id (const goto_program_templatet< codet, exprt > &p)

static irep_idt	loop_id (const_targett target)
	Human-readable loop name. More...

Public Attributes inherited from goto_program_templatet< codet, exprt >
instructionst	instructions
	The list of instructions in the goto program. More...

Detailed Description

A specialization of goto_program_templatet over goto programs in which instructions have codet type.

Definition at line 24 of file goto_program.h.

Member Typedef Documentation

◆ decl_identifierst

typedef std::set<irep_idt> goto_programt::decl_identifierst

Definition at line 64 of file goto_program.h.

Constructor & Destructor Documentation

◆ goto_programt() [1/3]

goto_programt::goto_programt ( )

inline

Definition at line 39 of file goto_program.h.

◆ goto_programt() [2/3]

goto_programt::goto_programt ( const goto_programt & )

delete

◆ goto_programt() [3/3]

goto_programt::goto_programt ( goto_programt && other )

inline

Definition at line 52 of file goto_program.h.

Member Function Documentation

◆ get_decl_identifiers()

void goto_programt::get_decl_identifiers ( decl_identifierst & decl_identifiers ) const

Definition at line 218 of file goto_program.cpp.

References forall_goto_program_instructions, and to_symbol_expr().

Referenced by invariant_propagationt::add_objects(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), and get_local_identifiers().

◆ operator=() [1/2]

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

delete

◆ operator=() [2/2]

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

inline

Definition at line 57 of file goto_program.h.

References goto_program_templatet< codeT, guardT >::operator=().

◆ output_instruction() [1/2]

std::ostream & goto_programt::output_instruction	(	const class namespacet &	ns,
		const irep_idt &	identifier,
		std::ostream &	out,
		instructionst::const_iterator	it
	)		const

See below.

Parameters

ns	the namespace to resolve the expressions in
identifier	the identifier used to find a symbol to identify the source language
out	the stream to write the goto string to
it	an iterator pointing to the instruction to convert

Returns: See below.

Definition at line 27 of file goto_program.cpp.

Referenced by enumerating_loop_accelerationt::accelerate(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), add_to_json(), goto_instrument_parse_optionst::doit(), goto_inlinet::expand_function_call(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), static_analysis_baset::output(), ai_baset::output(), output_dead_plain(), unified_difft::output_diff(), change_impactt::output_instruction(), ai_baset::output_json(), output_path(), ai_baset::output_xml(), and goto_unwindt::unwind().

◆ output_instruction() [2/2]

std::ostream& goto_programt::output_instruction	(	const class namespacet &	ns,
		const irep_idt &	identifier,
		std::ostream &	out,
		const instructiont &	instruction
	)		const

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

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

Public Types

Public Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ decl_identifierst

Constructor & Destructor Documentation

◆ goto_programt() [1/3]

◆ goto_programt() [2/3]

◆ goto_programt() [3/3]

Member Function Documentation

◆ get_decl_identifiers()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ output_instruction() [1/2]

◆ output_instruction() [2/2]