goto_loop_invariant_combinedt Class Reference

Handles the Branch 1 (invariant inductivity check) for one function in the combined –loop-invariant + –k-induction mode. More...

#include <goto_loop_invariant.h>

Inheritance diagram for goto_loop_invariant_combinedt:

Public Member Functions
	goto_loop_invariant_combinedt (const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function)
Public Member Functions inherited from goto_loopst
	goto_loopst (const irep_idt &_function_name, goto_functionst &_goto_functions, goto_functiont &_goto_function)
void	find_function_loops ()
void	dump () const
const function_loopst &	get_loops () const
function_loopst &	get_loops ()

Additional Inherited Members
Protected Types inherited from goto_loopst
typedef std::list< loopst >	function_loopst
Protected Member Functions inherited from goto_loopst
void	create_function_loop (goto_programt::instructionst::iterator loop_head, goto_programt::instructionst::iterator loop_exit)
void	get_modified_variables (goto_programt::instructionst::iterator instruction, function_loopst::iterator loop, std::vector< irep_idt > &function_name)
bool	compute_function_summary (const irep_idt &fname, std::vector< irep_idt > &in_progress, function_summaryt &out)
	Compute (or fetch the cached) summary of fname.
bool	summarise_call (const code_function_call2t &call, std::vector< irep_idt > &in_progress, function_summaryt &local, std::vector< expr2tc > &written_ptrs)
	Fold a call inside a callee into that callee's summary.
void	collect_address_taken (const expr2tc &expr, function_summaryt &out) const
	A variable whose address the callee takes can be reassigned through that address, which collect_lhs_symbols does not see.
void	collect_loop_symbols (const expr2tc &expr, loopst::loop_varst &out) const
	Collect the leaf symbols of expr into out, applying check_var_name.
void	collect_lhs_symbols (const expr2tc &expr, function_summaryt &out) const
	Walk an assignment LHS, classifying each leaf symbol: storage that is actually written goes to modified, sub-expressions used to locate that storage (pointer in *p, index in arr[i]) go to unmodified.
void	add_modified_var (loopst &loop, const expr2tc &expr)
void	add_unmodified_var (loopst &loop, const expr2tc &expr)
void	add_loop_var (loopst &loop, const expr2tc &expr, bool is_modified)
Static Protected Member Functions inherited from goto_loopst
static void	merge_summary (const function_summaryt &from, function_summaryt &out)
static void	note_pointer_write (const expr2tc &target, function_summaryt &local, std::vector< expr2tc > &written_ptrs)
static void	apply_callee_summary (loopst &loop, const function_summaryt &summary, const code_function_call2t &call)
Protected Attributes inherited from goto_loopst
irep_idt	function_name
goto_functionst &	goto_functions
goto_functiont &	goto_function
function_loopst	function_loops
std::unordered_map< irep_idt, function_summaryt, irep_id_hash >	function_summary_cache

Detailed Description

Handles the Branch 1 (invariant inductivity check) for one function in the combined –loop-invariant + –k-induction mode.

For each loop that carries a LOOP_INVARIANT annotation the pass inserts a non-deterministic verification branch before the original loop:

IF !nondet_bool() GOTO original_loop_head [skip Branch 1] ASSERT(INV) [base case – tagged property="invariant-base-case"] HAVOC(loop_vars) ASSUME(INV) ASSUME(loop_entry_cond) <copy of one loop-body iteration> ASSERT(INV) [step case – tagged property="invariant-inductive-step"] ASSUME(false) [terminate Branch 1 – never fall through] original_loop_head: [unchanged; k-induction will transform this]

The branch uses std::list::splice() rather than insert_swap() so that existing backward-GOTO targets (which point to original_loop_head) are not disturbed.

Constructor & Destructor Documentation

goto_loop_invariant_combinedt()

goto_loop_invariant_combinedt::goto_loop_invariant_combinedt ( const irep_idt & _function_name, goto_functionst & _goto_functions, goto_functiont & _goto_function )

inline

---

The documentation for this class was generated from the following files:

• src/goto-programs/goto_loop_invariant.h
• src/goto-programs/goto_loop_invariant.cpp