scratch_programt Member List

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

add(instructiont &&instruction)	goto_programt	inline
add_instruction()	goto_programt	inline
add_instruction(goto_program_instruction_typet type)	goto_programt	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, guard_managert &guard_manager)	scratch_programt
check_sat(guard_managert &guard_manager)	scratch_programt	inline
checker	scratch_programt	protected
clear()	goto_programt	inline
compute_incoming_edges()	goto_programt
compute_location_numbers(unsigned &nr)	goto_programt	inline
compute_location_numbers()	goto_programt	inline
compute_loop_numbers()	goto_programt
compute_target_numbers()	goto_programt
const_cast_target(const_targett t)	goto_programt	inline
const_cast_target(const_targett t) const	goto_programt	inline
const_targetst typedef	goto_programt
const_targett typedef	goto_programt
constant_propagation	scratch_programt
copy_from(const goto_programt &src)	goto_programt
decl_identifierst typedef	goto_programt
destructive_append(goto_programt &p)	goto_programt	inline
destructive_insert(const_targett target, goto_programt &p)	goto_programt	inline
empty() const	goto_programt	inline
equals(const goto_programt &other) const	goto_programt
equation	scratch_programt	protected
eval(const exprt &e)	scratch_programt
fix_types()	scratch_programt
functions	scratch_programt	protected
get_decl_identifiers(decl_identifierst &decl_identifiers) const	goto_programt
get_default_options()	scratch_programt	protectedstatic
get_end_function()	goto_programt	inline
get_end_function() const	goto_programt	inline
get_successors(Target target) const	goto_programt
goto_programt(const goto_programt &)=delete	goto_programt
goto_programt(goto_programt &&other)	goto_programt	inline
goto_programt()	goto_programt	inline
has_assertion() const	goto_programt
insert_after(const_targett target)	goto_programt	inline
insert_after(const_targett target, const instructiont &i)	goto_programt	inline
insert_before(const_targett target)	goto_programt	inline
insert_before(const_targett target, const instructiont &i)	goto_programt	inline
insert_before_swap(targett target)	goto_programt	inline
insert_before_swap(targett target, instructiont &instruction)	goto_programt	inline
insert_before_swap(targett target, goto_programt &p)	goto_programt	inline
instructions	goto_programt
instructionst typedef	goto_programt
loop_id(const irep_idt &function_id, const instructiont &instruction)	goto_programt	inlinestatic
make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_atomic_begin(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_atomic_end(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_catch(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_end_function(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_function_call(exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_goto(targett _target, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_incomplete_goto(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_incomplete_goto(const code_gotot &, const source_locationt &=source_locationt::nil())	goto_programt	static
make_location(const source_locationt &l)	goto_programt	inlinestatic
make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_set_return_value(const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete	goto_programt	static
make_skip(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
make_throw(const source_locationt &l=source_locationt::nil())	goto_programt	inlinestatic
ns	scratch_programt	protected
operator=(const goto_programt &)=delete	goto_programt
operator=(goto_programt &&other)	goto_programt	inline
options	scratch_programt	protected
output(std::ostream &out) const	goto_programt
path_storage	scratch_programt	protected
satcheck	scratch_programt	protected
satchecker	scratch_programt	protected
scratch_programt(symbol_table_baset &_symbol_table, message_handlert &mh, guard_managert &guard_manager)	scratch_programt	inline
swap(goto_programt &program)	goto_programt	inline
symbol_table	scratch_programt	protected
symex	scratch_programt	protected
symex_state	scratch_programt	protected
symex_symbol_table	scratch_programt	protected
target_less_than typedef	goto_programt
targetst typedef	goto_programt
targett typedef	goto_programt
update()	goto_programt
validate(const namespacet &ns, const validation_modet vm) const	goto_programt	inline
z3	scratch_programt	protected
~goto_programt()	goto_programt	inline