CBMC
|
This is the complete list of members for acceleratet, including all inherited members.
accelerate_limit | acceleratet | static |
accelerate_loop(goto_programt::targett &loop_header) | acceleratet | |
accelerate_loops() | acceleratet | |
accelerate_path(patht &path, path_acceleratort &accelerator) | acceleratet | |
acceleratet(goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3, guard_managert &guard_manager) | acceleratet | inline |
add_dirty_checks() | acceleratet | protected |
build_state_machine(trace_automatont::sym_mapt::iterator p, trace_automatont::sym_mapt::iterator end, state_sett &accept_states, symbol_exprt state, symbol_exprt next_state, scratch_programt &state_machine) | acceleratet | protected |
contains_nested_loops(goto_programt::targett &loop_header) | acceleratet | protected |
decl(symbol_exprt &sym, goto_programt::targett t) | acceleratet | protected |
decl(symbol_exprt &sym, goto_programt::targett t, exprt init) | acceleratet | protected |
dirty_vars_map | acceleratet | protected |
extend_path(goto_programt::targett &t, goto_programt::targett &loop_header, natural_loops_mutablet::natural_loopt &loop, patht &prefix, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump) | acceleratet | protected |
find_back_jump(goto_programt::targett loop_header) | acceleratet | protected |
find_paths(goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump) | acceleratet | protected |
goto_functions | acceleratet | protected |
guard_manager | acceleratet | protected |
insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path) | acceleratet | protected |
insert_automaton(trace_automatont &automaton) | acceleratet | protected |
insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path) | acceleratet | protected |
is_underapproximate(path_acceleratort &accelerator) | acceleratet | protected |
make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc) | acceleratet | protected |
make_symbol(std::string name, typet type) | acceleratet | protected |
message_handler | acceleratet | protected |
natural_loops | acceleratet | protected |
ns | acceleratet | protected |
overflow_locs | acceleratet | protected |
overflow_mapt typedef | acceleratet | protected |
program | acceleratet | protected |
restrict_traces() | acceleratet | |
set_dirty_vars(path_acceleratort &accelerator) | acceleratet | protected |
subsumed | acceleratet | protected |
symbol_table | acceleratet | protected |
use_z3 | acceleratet | protected |
utils | acceleratet | protected |