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) | scratch_programt | |
check_sat() | 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 |
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_end_function() | goto_programt | inline |
get_end_function() const | goto_programt | inline |
get_function_id(const_targett l) | goto_programt | inlinestatic |
get_function_id(const goto_programt &p) | goto_programt | inlinestatic |
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_before(const_targett target) | 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 instructiont &instruction) | 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(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const | goto_programt | |
output(std::ostream &out) const | goto_programt | inline |
output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const | goto_programt | |
path_storage | scratch_programt | protected |
satcheck | scratch_programt | protected |
satchecker | scratch_programt | protected |
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh) | 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 |
targetst typedef | goto_programt | |
targett typedef | goto_programt | |
update() | goto_programt | |
update_instructions_function(const irep_idt &function_id) | goto_programt | inline |
z3 | scratch_programt | protected |
~goto_programt() | goto_programt | inline |