CBMC
acceleration_utilst Member List

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_utilstinline
acceleration_utilst(symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)acceleration_utilstinline
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 typedefacceleration_utilst
expr_pairt typedefacceleration_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_functionsacceleration_utilst
loop_counteracceleration_utilst
message_handleracceleration_utilstprotected
nilacceleration_utilst
nsacceleration_utilst
polynomial_array_assignmentst typedefacceleration_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_tableacceleration_utilst