cprover
scratch_programt Class Reference

#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_programtoperator= (const goto_programt &)=delete
 
 goto_programt (goto_programt &&other)
 
goto_programtoperator= (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_tabletsymbol_table
 
symbol_tablet symex_symbol_table
 
namespacet ns
 
symex_target_equationt equation
 
path_fifot path_storage
 
optionst options
 
goto_symext symex
 
std::unique_ptr< proptsatcheck
 
bv_pointerst satchecker
 
smt2_dect z3
 
prop_convtchecker
 

Additional Inherited Members

- Public Types inherited from goto_programt
typedef std::list< instructiontinstructionst
 
typedef instructionst::iterator targett
 
typedef instructionst::const_iterator const_targett
 
typedef std::list< targetttargetst
 
typedef std::list< const_targettconst_targetst
 
typedef std::set< irep_idtdecl_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 program)

Definition at line 171 of file scratch_program.cpp.

◆ append() [2/2]

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

Definition at line 72 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 ( )
inline

Definition at line 65 of file scratch_program.h.

◆ check_sat() [2/2]

bool scratch_programt::check_sat ( bool  do_slice)

Definition at line 25 of file scratch_program.cpp.

◆ 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: