cprover
scratch_programt Member List

This is the complete list of members for scratch_programt, including all inherited members.

add_instruction()goto_program_templatet< codet, exprt >inline
add_instruction(goto_program_instruction_typet type)goto_program_templatet< codet, exprt >inline
append(goto_programt::instructionst &instructions)scratch_programt
append(goto_programt &program)scratch_programt
append_loop(goto_programt &program, goto_programt::targett loop_header)scratch_programt
append_path(patht &path)scratch_programt
assign(const exprt &lhs, const exprt &rhs)scratch_programt
assume(const exprt &guard)scratch_programt
check_sat(bool do_slice)scratch_programt
check_sat()scratch_programtinline
checkerscratch_programtprotected
clear()goto_program_templatet< codet, exprt >inline
compute_incoming_edges()goto_program_templatet< codet, exprt >
compute_location_numbers(unsigned &nr)goto_program_templatet< codet, exprt >inline
compute_location_numbers()goto_program_templatet< codet, exprt >inline
compute_loop_numbers()goto_program_templatet< codet, exprt >
compute_target_numbers()goto_program_templatet< codet, exprt >
const_cast_target(const_targett t)goto_program_templatet< codet, exprt >inline
const_cast_target(const_targett t) constgoto_program_templatet< codet, exprt >inline
const_targetst typedefgoto_program_templatet< codet, exprt >
const_targett typedefgoto_program_templatet< codet, exprt >
constant_propagationscratch_programt
copy_from(const goto_program_templatet< codet, exprt > &src)goto_program_templatet< codet, exprt >
decl_identifierst typedefgoto_programt
destructive_append(goto_program_templatet< codet, exprt > &p)goto_program_templatet< codet, exprt >inline
destructive_insert(const_targett target, goto_program_templatet< codet, exprt > &p)goto_program_templatet< codet, exprt >inline
empty() constgoto_program_templatet< codet, exprt >inline
equationscratch_programtprotected
eval(const exprt &e)scratch_programt
fix_types()scratch_programt
functionsscratch_programtprotected
get_decl_identifiers(decl_identifierst &decl_identifiers) constgoto_programt
get_end_function()goto_program_templatet< codet, exprt >inline
get_function_id(const_targett l)goto_program_templatet< codet, exprt >inlinestatic
get_function_id(const goto_program_templatet< codet, exprt > &p)goto_program_templatet< codet, exprt >inlinestatic
get_successors(Target target) constgoto_program_templatet< codet, exprt >
goto_program_templatet(const goto_program_templatet &)=deletegoto_program_templatet< codet, exprt >
goto_program_templatet(goto_program_templatet &&other)goto_program_templatet< codet, exprt >inline
goto_program_templatet()goto_program_templatet< codet, exprt >inline
goto_programt()goto_programtinline
goto_programt(const goto_programt &)=deletegoto_programt
goto_programt(goto_programt &&other)goto_programtinline
has_assertion() constgoto_program_templatet< codet, exprt >
insert_after(const_targett target)goto_program_templatet< codet, exprt >inline
insert_before(const_targett target)goto_program_templatet< codet, exprt >inline
insert_before_swap(targett target)goto_program_templatet< codet, exprt >inline
insert_before_swap(targett target, instructiont &instruction)goto_program_templatet< codet, exprt >inline
insert_before_swap(targett target, goto_program_templatet< codet, exprt > &p)goto_program_templatet< codet, exprt >inline
instructionsgoto_program_templatet< codet, exprt >
instructionst typedefgoto_program_templatet< codet, exprt >
loop_id(const_targett target)goto_program_templatet< codet, exprt >inlinestatic
nsscratch_programtprotected
operator=(const goto_programt &)=deletegoto_programt
operator=(goto_programt &&other)goto_programtinline
goto_program_templatet< codet, exprt >::operator=(const goto_program_templatet &)=deletegoto_program_templatet< codet, exprt >
goto_program_templatet< codet, exprt >::operator=(goto_program_templatet &&other)goto_program_templatet< codet, exprt >inline
output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) constgoto_program_templatet< codet, exprt >
output(std::ostream &out) constgoto_program_templatet< codet, exprt >inline
output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) constgoto_programt
output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructiont &instruction) constgoto_programt
goto_program_templatet< codet, exprt >::output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const=0goto_program_templatet< codet, exprt >pure virtual
satcheckscratch_programtprotected
satcheckerscratch_programtprotected
scratch_programt(symbol_tablet &_symbol_table)scratch_programtinlineexplicit
swap(goto_program_templatet< codet, exprt > &program)goto_program_templatet< codet, exprt >inline
symbol_tablescratch_programtprotected
symexscratch_programtprotected
symex_statescratch_programtprotected
targetst typedefgoto_program_templatet< codet, exprt >
targett typedefgoto_program_templatet< codet, exprt >
update()goto_program_templatet< codet, exprt >
z3scratch_programtprotected
~goto_program_templatet()goto_program_templatet< codet, exprt >inlinevirtual
~scratch_programt()scratch_programtinline