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)
 
 ~scratch_programt ()
 
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
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_programtoperator= (const goto_programt &)=delete
 
 goto_programt (goto_programt &&other)
 
goto_programtoperator= (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_templatetoperator= (const goto_program_templatet &)=delete
 
goto_program_templatetoperator= (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...
 

Public Attributes

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

Protected Attributes

goto_symex_statet symex_state
 
goto_functionst functions
 
symbol_tabletsymbol_table
 
const namespacet ns
 
symex_target_equationt equation
 
goto_symext symex
 
proptsatcheck
 
bv_pointerst satchecker
 
smt2_dect z3
 
prop_convtchecker
 

Additional Inherited Members

- Public Types inherited from goto_programt
typedef std::set< irep_idtdecl_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< targetttargetst
 
typedef std::list< const_targettconst_targetst
 
- 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...
 

Detailed Description

Definition at line 32 of file scratch_program.h.

Constructor & Destructor Documentation

◆ scratch_programt()

scratch_programt::scratch_programt ( symbol_tablet _symbol_table)
inlineexplicit

Definition at line 35 of file scratch_program.h.

◆ ~scratch_programt()

scratch_programt::~scratch_programt ( )
inline

Definition at line 48 of file scratch_program.h.

References satcheck.

Member Function Documentation

◆ append() [1/2]

◆ append() [2/2]

◆ append_loop()

◆ append_path()

◆ assign()

◆ assume()

◆ check_sat() [1/2]

◆ check_sat() [2/2]

bool scratch_programt::check_sat ( )
inline

Definition at line 63 of file scratch_program.h.

◆ eval()

◆ fix_types()

Member Data Documentation

◆ checker

prop_convt* scratch_programt::checker
protected

Definition at line 85 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ constant_propagation

bool scratch_programt::constant_propagation

Definition at line 72 of file scratch_program.h.

Referenced by check_sat().

◆ equation

symex_target_equationt scratch_programt::equation
protected

Definition at line 79 of file scratch_program.h.

Referenced by check_sat().

◆ functions

goto_functionst scratch_programt::functions
protected

Definition at line 76 of file scratch_program.h.

Referenced by check_sat().

◆ ns

const namespacet scratch_programt::ns
protected

Definition at line 78 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ satcheck

propt* scratch_programt::satcheck
protected

Definition at line 82 of file scratch_program.h.

Referenced by ~scratch_programt().

◆ satchecker

bv_pointerst scratch_programt::satchecker
protected

Definition at line 83 of file scratch_program.h.

◆ symbol_table

symbol_tablet& scratch_programt::symbol_table
protected

Definition at line 77 of file scratch_program.h.

◆ symex

goto_symext scratch_programt::symex
protected

Definition at line 80 of file scratch_program.h.

Referenced by check_sat().

◆ symex_state

goto_symex_statet scratch_programt::symex_state
protected

Definition at line 75 of file scratch_program.h.

Referenced by check_sat(), and eval().

◆ z3

smt2_dect scratch_programt::z3
protected

Definition at line 84 of file scratch_program.h.


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