goto_loop_invariantt Member List

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

active_frame_enforcer	goto_loop_invariantt	protected
active_loop_assigns	goto_loop_invariantt	protected
add_loop_var(loopst &loop, const expr2tc &expr, bool is_modified)	goto_loopst	protected
add_modified_var(loopst &loop, const expr2tc &expr)	goto_loopst	protected
add_unmodified_var(loopst &loop, const expr2tc &expr)	goto_loopst	protected
apply_callee_summary(loopst &loop, const function_summaryt &summary, const code_function_call2t &call)	goto_loopst	protectedstatic
collect_address_taken(const expr2tc &expr, function_summaryt &out) const	goto_loopst	protected
collect_lhs_symbols(const expr2tc &expr, function_summaryt &out) const	goto_loopst	protected
collect_loop_symbols(const expr2tc &expr, loopst::loop_varst &out) const	goto_loopst	protected
collect_symbols(const expr2tc &expr, std::set< irep_idt > &symbols)	goto_loop_invariantt	protectedstatic
compute_function_summary(const irep_idt &fname, std::vector< irep_idt > &in_progress, function_summaryt &out)	goto_loopst	protected
context	goto_loop_invariantt	protected
convert_loop_with_invariant(loopst &loop)	goto_loop_invariantt	protected
create_function_loop(goto_programt::instructionst::iterator loop_head, goto_programt::instructionst::iterator loop_exit)	goto_loopst	protected
dump() const	goto_loopst
extract_and_remove_side_effects(goto_programt::targett loop_head, const loopst &loop, const std::vector< expr2tc > &invariants, goto_programt &side_effects_out)	goto_loop_invariantt	protected
extract_loop_assigns(const loopst &loop)	goto_loop_invariantt	protected
extract_loop_invariants(const loopst &loop)	goto_loop_invariantt	protected
find_function_loops()	goto_loopst
function_loops	goto_loopst	protected
function_loopst typedef	goto_loopst	protected
function_name	goto_loopst	protected
function_summary_cache	goto_loopst	protected
get_loops() const	goto_loopst	inline
get_loops()	goto_loopst	inline
get_modified_variables(goto_programt::instructionst::iterator instruction, function_loopst::iterator loop, std::vector< irep_idt > &function_name)	goto_loopst	protected
goto_function	goto_loopst	protected
goto_functions	goto_loopst	protected
goto_loop_invariant()	goto_loop_invariantt	protected
goto_loop_invariantt(const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function, contextt &_context, bool _use_frame_rule)	goto_loop_invariantt	inline
goto_loopst(const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function)	goto_loopst	inline
havoc_pointee_type(const expr2tc &ptr, const namespacet &ns)	goto_loop_invariantt	protectedstatic
havoc_pointees(const loopst &loop, const locationt &loc, goto_programt &dest) const	goto_loop_invariantt	protected
insert_assert_before_loop(goto_programt::targett &loop_head, const std::vector< expr2tc > &invariants, const goto_programt &side_effects)	goto_loop_invariantt	protected
insert_havoc_and_assume_before_condition(goto_programt::targett loop_head, const loopst &loop, const std::vector< expr2tc > &invariants, const std::vector< expr2tc > &loop_assigns, goto_programt &side_effects)	goto_loop_invariantt	protected
insert_inductive_step_and_termination(const loopst &loop, const std::vector< expr2tc > &invariants, const goto_programt &side_effects)	goto_loop_invariantt	protected
kMaxHavocPointeeBits	goto_loop_invariantt	protectedstatic
kMaxInvariantSearchBack	goto_loop_invariantt	static
merge_summary(const function_summaryt &from, function_summaryt &out)	goto_loopst	protectedstatic
note_pointer_write(const expr2tc &target, function_summaryt &local, std::vector< expr2tc > &written_ptrs)	goto_loopst	protectedstatic
pointees_havocable(const loopst &loop) const	goto_loop_invariantt	protected
summarise_call(const code_function_call2t &call, std::vector< irep_idt > &in_progress, function_summaryt &local, std::vector< expr2tc > &written_ptrs)	goto_loopst	protected
use_frame_rule	goto_loop_invariantt	protected