CBMC
|
This is the complete list of members for acceleration_utilst, including all inherited members.
abstract_arrays(exprt &expr, expr_mapt &abstractions) | acceleration_utilst | |
acceleration_utilst(symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter) | acceleration_utilst | inline |
acceleration_utilst(symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions) | acceleration_utilst | inline |
array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices) | acceleration_utilst | |
assign_array(const index_exprt &lhs, const exprt &rhs, scratch_programt &program) | acceleration_utilst | |
check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager) | acceleration_utilst | |
do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program) | acceleration_utilst | |
do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager) | acceleration_utilst | |
do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program) | acceleration_utilst | |
ensure_no_overflows(scratch_programt &program) | acceleration_utilst | |
expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly) | acceleration_utilst | |
expr_pairst typedef | acceleration_utilst | |
expr_pairt typedef | acceleration_utilst | |
extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial) | acceleration_utilst | |
find_modified(const patht &path, expr_sett &modified) | acceleration_utilst | |
find_modified(const goto_programt &program, expr_sett &modified) | acceleration_utilst | |
find_modified(const goto_programt::instructionst &instructions, expr_sett &modified) | acceleration_utilst | |
find_modified(const natural_loops_mutablet::natural_loopt &loop, expr_sett &modified) | acceleration_utilst | |
find_modified(goto_programt::const_targett t, expr_sett &modified) | acceleration_utilst | |
fresh_symbol(std::string base, typet type) | acceleration_utilst | |
gather_array_accesses(const exprt &expr, expr_sett &arrays) | acceleration_utilst | |
gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written) | acceleration_utilst | |
gather_rvalues(const exprt &expr, expr_sett &rvalues) | acceleration_utilst | |
goto_functions | acceleration_utilst | |
loop_counter | acceleration_utilst | |
message_handler | acceleration_utilst | protected |
nil | acceleration_utilst | |
ns | acceleration_utilst | |
polynomial_array_assignmentst typedef | acceleration_utilst | |
precondition(patht &path) | acceleration_utilst | |
push_nondet(exprt &expr) | acceleration_utilst | |
stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path) | acceleration_utilst | |
stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution) | acceleration_utilst | |
symbol_table | acceleration_utilst |