goto_loop_invariant.h File Reference

#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_loops.h>
#include <irep2/irep2_guard.h>
#include <util/symtab/context.h>
#include <irep2/irep2_expr.h>
#include <set>
#include <unordered_set>
#include <vector>

Include dependency graph for goto_loop_invariant.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

Namespaces
namespace	loop_invariant

Functions
bool	loop_invariant::is_inert_scan_instruction (goto_programt::const_targett t)
	Instructions with no effect a caller needs to account for: no write to a tracked variable, no control-flow or heap/external effect.
void	goto_loop_invariant (goto_functionst &goto_functions, contextt &context, bool use_frame_rule)
	Entry point: process loop invariants for all functions.
void	goto_loop_invariant_combined (goto_functionst &goto_functions)
	Combined loop-invariant + k-induction mode.

Variables
const char *const	kSynthesisedInvariantProperty
	Property tag that goto_synthesise_loop_invariants stamps on the LOOP_INVARIANT markers it emits.

Function Documentation

goto_loop_invariant()

void goto_loop_invariant	(	goto_functionst &	goto_functions,
		contextt &	context,
		bool	use_frame_rule )

Entry point: process loop invariants for all functions.

When use_frame_rule is true, enables the observational frame rule (Snapshot → Havoc → Assume) for enhanced inductive verification.

goto_loop_invariant_combined()

void goto_loop_invariant_combined

(

goto_functionst &

goto_functions

)

Combined loop-invariant + k-induction mode.

Inserts a non-deterministic "Branch 1" verification block immediately before each annotated loop. Branch 1 checks that the user-supplied invariant is actually inductive (base case + inductive step), using specially tagged ASSERT instructions so the verifier can distinguish invariant failures from ordinary program assertion failures.

The original loop is left untouched for subsequent transformation by goto_k_induction (Branch 2), which adds ASSUME(invariant) after its nondet-assign step to tighten the inductive-step search space.

Variable Documentation

kSynthesisedInvariantProperty

const char* const kSynthesisedInvariantProperty

extern

Property tag that goto_synthesise_loop_invariants stamps on the LOOP_INVARIANT markers it emits.

The extractor here accepts a tagged marker only when it sits immediately before the loop head it is being extracted for; a user-written __ESBMC_loop_invariant carries no tag and keeps the looser proximity rule. Without the tag the two passes share nothing but a 10-instruction window, and a synthesised invariant silently attaches itself to whichever loop happens to be nearby.