cprover
scratch_programt Class Reference

#include <scratch_program.h>

Inheritance diagram for scratch_programt:
[legend]
Collaboration diagram for scratch_programt:
[legend]

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
 
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_programt &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_programt &p)
 Appends the given program, which is destroyed. More...
 
void destructive_insert (const_targett target, goto_programt &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...
 
std::ostream & output_instruction (const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) 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 ()
 
const_targett get_end_function () const
 
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...
 

Public Attributes

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

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)
 
static const irep_idt get_function_id (const goto_programt &p)
 
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.

References options, and optionst::set_option().

Member Function Documentation

◆ append() [1/2]

◆ append() [2/2]

void scratch_programt::append ( goto_programt program)

◆ append_loop()

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

◆ append_path()

void scratch_programt::append_path ( patht path)

◆ assign()

◆ assume()

◆ check_sat() [1/2]

◆ check_sat() [2/2]

bool scratch_programt::check_sat ( )
inline

Definition at line 68 of file scratch_program.h.

◆ eval()

◆ fix_types()

Member Data Documentation

◆ checker

prop_convt* scratch_programt::checker
protected

Definition at line 93 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ constant_propagation

bool scratch_programt::constant_propagation

Definition at line 77 of file scratch_program.h.

Referenced by check_sat().

◆ equation

symex_target_equationt scratch_programt::equation
protected

Definition at line 85 of file scratch_program.h.

Referenced by check_sat().

◆ functions

goto_functionst scratch_programt::functions
protected

Definition at line 81 of file scratch_program.h.

Referenced by check_sat().

◆ ns

namespacet scratch_programt::ns
protected

Definition at line 84 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ options

optionst scratch_programt::options
protected

Definition at line 87 of file scratch_program.h.

Referenced by scratch_programt().

◆ path_storage

path_fifot scratch_programt::path_storage
protected

Definition at line 86 of file scratch_program.h.

◆ satcheck

std::unique_ptr<propt> scratch_programt::satcheck
protected

Definition at line 90 of file scratch_program.h.

◆ satchecker

bv_pointerst scratch_programt::satchecker
protected

Definition at line 91 of file scratch_program.h.

◆ symbol_table

symbol_tablet& scratch_programt::symbol_table
protected

Definition at line 82 of file scratch_program.h.

◆ symex

goto_symext scratch_programt::symex
protected

Definition at line 88 of file scratch_program.h.

Referenced by check_sat().

◆ symex_state

goto_symex_statet scratch_programt::symex_state
protected

Definition at line 80 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ symex_symbol_table

symbol_tablet scratch_programt::symex_symbol_table
protected

Definition at line 83 of file scratch_program.h.

Referenced by check_sat().

◆ z3

smt2_dect scratch_programt::z3
protected

Definition at line 92 of file scratch_program.h.


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