goto_k_induction.h File Reference

#include <goto-programs/goto_functions.h>
#include <util/symtab/namespace.h>

Include dependency graph for goto_k_induction.h:

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

Go to the source code of this file.

Functions
bool	goto_k_induction (goto_functionst &goto_functions, const namespacet &ns, bool continue_past_failed_assertions)
	Per-loop k-induction transformation: havoc each loop's modified variables and inject an ASSUME of the loop entry condition right before the loop head.

Function Documentation

goto_k_induction()

bool goto_k_induction	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		bool	continue_past_failed_assertions )

Per-loop k-induction transformation: havoc each loop's modified variables and inject an ASSUME of the loop entry condition right before the loop head.

Applied to every function with a body (including __ESBMC_main, which is loop-free and therefore untouched, and library helpers).

A loop that writes through a pointer also havocs that storage: *p while the loop leaves p alone, otherwise the named objects the whole-program Andersen analysis resolves the pointer to. Returns true, after logging why, when the inductive step would be unsound: a write in a reachable user function can be covered neither way (issues #5224, #5230), a reachable call to __VERIFIER_nondet_memory (#5593), or a loop that allocates under a leak check. The caller must then disable the inductive step. continue_past_failed_assertions is set when claims past a violation are still checked (–multi-property, coverage), so that a path through a failed assertion still counts as entering the loop (#7900).