#include <scratch_program.h>

Inheritance diagram for scratch_programt:

Collaboration diagram for scratch_programt:

Public Member Functions
	scratch_programt (symbol_tablet &_symbol_table, message_handlert &mh)

void	append (goto_programt::instructionst &instructions)

void	append (goto_programt &program)

void	append_path (patht &path)

void	append_loop (goto_programt &program, goto_programt::targett loop_header)

targett	assign (const exprt &lhs, const exprt &rhs)

targett	assume (const exprt &guard)

bool	check_sat (bool do_slice)

bool	check_sat ()

exprt	eval (const exprt &e)

void	fix_types ()

Public Member Functions inherited from goto_programt
	goto_programt (const goto_programt &)=delete
	Copying is deleted as this class contains pointers that cannot be copied. More...

goto_programt &	operator= (const goto_programt &)=delete

	goto_programt (goto_programt &&other)

goto_programt &	operator= (goto_programt &&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...

template<typename Target >
std::list< Target >	get_successors (Target target) const
	Get control-flow successors of a given instruction. More...

void	compute_incoming_edges ()
	Compute for each instruction the set of instructions it is a successor of. More...

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_programt &p)
	Insertion that preserves jumps to "target". More...

targett	insert_before (const_targett target)
	Insertion before the instruction pointed-to by the given instruction iterator `target`. More...

targett	insert_after (const_targett target)
	Insertion after the instruction pointed-to by the given instruction iterator `target`. More...

void	destructive_append (goto_programt &p)
	Appends the given program `p` to `*this`. `p` is destroyed. More...

void	destructive_insert (const_targett target, goto_programt &p)
	Inserts the given program `p` before `target`. 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...

std::ostream &	output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
	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	update_instructions_function (const irep_idt &function_id)
	Sets the `function` member of each instruction if not yet set Note that a goto program need not be a goto function and therefore, we cannot do this in update(), but only at the level of of goto_functionst where goto programs are guaranteed to be named functions. 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...

	goto_programt ()
	Constructor. More...

	~goto_programt ()

void	swap (goto_programt &program)
	Swap the goto program. More...

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

targett	get_end_function ()
	Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More...

const_targett	get_end_function () const
	Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program. More...

void	copy_from (const goto_programt &src)
	Copy a full goto program, preserving targets. More...

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

void	get_decl_identifiers (decl_identifierst &decl_identifiers) const
	get the variables in decl statements More...

bool	equals (const goto_programt &other) const
	Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instructions, each pair of instructions compares equal, and relative jumps have the same distance. More...

void	validate (const namespacet &ns, const validation_modet vm) const
	Check that the goto program is well-formed. More...

Public Attributes
bool	constant_propagation

Public Attributes inherited from goto_programt
instructionst	instructions
	The list of instructions in the goto program. More...

Static Protected Member Functions
static optionst	get_default_options ()

Protected Attributes
goto_symex_statet	symex_state

goto_functionst	functions

symbol_tablet &	symbol_table

symbol_tablet	symex_symbol_table

namespacet	ns

symex_target_equationt	equation

path_fifot	path_storage

optionst	options

goto_symext	symex

std::unique_ptr< propt >	satcheck

bv_pointerst	satchecker

smt2_dect	z3

prop_convt *	checker

Additional Inherited Members
Public Types inherited from goto_programt
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

typedef std::set< irep_idt >	decl_identifierst

Static Public Member Functions inherited from goto_programt
static const irep_idt	get_function_id (const_targett l)
	Get the id of the function that contains the instruction pointed-to by the given instruction iterator. More...

static const irep_idt	get_function_id (const goto_programt &p)
	Get the id of the function that contains the given goto program. More...

static irep_idt	loop_id (const instructiont &instruction)
	Human-readable loop name. More...

Detailed Description

Definition at line 36 of file scratch_program.h.

Constructor & Destructor Documentation

◆ scratch_programt()

scratch_programt::scratch_programt	(	symbol_tablet &	_symbol_table,
		message_handlert &	mh
	)

inline

Definition at line 39 of file scratch_program.h.

Member Function Documentation

◆ append() [1/2]

void scratch_programt::append ( goto_programt::instructionst & instructions )

Definition at line 72 of file scratch_program.cpp.

◆ append() [2/2]

void scratch_programt::append ( goto_programt & program )

Definition at line 171 of file scratch_program.cpp.

◆ append_loop()

void scratch_programt::append_loop	(	goto_programt &	program,
		goto_programt::targett	loop_header
	)

Definition at line 179 of file scratch_program.cpp.

◆ append_path()

void scratch_programt::append_path ( patht & path )

Definition at line 147 of file scratch_program.cpp.

◆ assign()

goto_programt::targett scratch_programt::assign	(	const exprt &	lhs,
		const exprt &	rhs
	)

Definition at line 80 of file scratch_program.cpp.

◆ assume()

goto_programt::targett scratch_programt::assume ( const exprt & guard )

Definition at line 91 of file scratch_program.cpp.

◆ check_sat() [1/2]

bool scratch_programt::check_sat ( bool do_slice )

Definition at line 25 of file scratch_program.cpp.

◆ check_sat() [2/2]

bool scratch_programt::check_sat ( )

inline

Definition at line 65 of file scratch_program.h.

◆ eval()

exprt scratch_programt::eval ( const exprt & e )

Definition at line 63 of file scratch_program.cpp.

◆ fix_types()

void scratch_programt::fix_types ( )

Definition at line 124 of file scratch_program.cpp.

◆ get_default_options()

optionst scratch_programt::get_default_options ( )

staticprotected

Definition at line 205 of file scratch_program.cpp.

Member Data Documentation

◆ checker

prop_convt* scratch_programt::checker

protected

Definition at line 90 of file scratch_program.h.

◆ constant_propagation

bool scratch_programt::constant_propagation

Definition at line 74 of file scratch_program.h.

◆ equation

symex_target_equationt scratch_programt::equation

protected

Definition at line 82 of file scratch_program.h.

◆ functions

goto_functionst scratch_programt::functions

protected

Definition at line 78 of file scratch_program.h.

◆ ns

namespacet scratch_programt::ns

protected

Definition at line 81 of file scratch_program.h.

◆ options

optionst scratch_programt::options

protected

Definition at line 84 of file scratch_program.h.

◆ path_storage

path_fifot scratch_programt::path_storage

protected

Definition at line 83 of file scratch_program.h.

◆ satcheck

std::unique_ptr<propt> scratch_programt::satcheck

protected

Definition at line 87 of file scratch_program.h.

◆ satchecker

bv_pointerst scratch_programt::satchecker

protected

Definition at line 88 of file scratch_program.h.

◆ symbol_table

symbol_tablet& scratch_programt::symbol_table

protected

Definition at line 79 of file scratch_program.h.

◆ symex

goto_symext scratch_programt::symex

protected

Definition at line 85 of file scratch_program.h.

◆ symex_state

goto_symex_statet scratch_programt::symex_state

protected

Definition at line 77 of file scratch_program.h.

◆ symex_symbol_table

symbol_tablet scratch_programt::symex_symbol_table

protected

Definition at line 80 of file scratch_program.h.

◆ z3

smt2_dect scratch_programt::z3

protected

Definition at line 89 of file scratch_program.h.

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

goto-instrument/accelerate/scratch_program.h
goto-instrument/accelerate/scratch_program.cpp

Public Member Functions

Public Attributes

Static Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ scratch_programt()

Member Function Documentation

◆ append() [1/2]

◆ append() [2/2]

◆ append_loop()

◆ append_path()

◆ assign()

◆ assume()

◆ check_sat() [1/2]

◆ check_sat() [2/2]

◆ eval()

◆ fix_types()

◆ get_default_options()

Member Data Documentation

◆ checker

◆ constant_propagation

◆ equation

◆ functions

◆ ns

◆ options

◆ path_storage

◆ satcheck

◆ satchecker

◆ symbol_table

◆ symex

◆ symex_state

◆ symex_symbol_table

◆ z3