goto_k_induction.cpp File Reference

#include <goto-programs/goto_k_induction.h>
#include <algorithm>
#include <array>
#include <functional>
#include <goto-programs/goto_loops.h>
#include <goto-programs/loopst.h>
#include <goto-programs/remove_no_op.h>
#include <irep2/irep2_expr.h>
#include <irep2/irep2_guard.h>
#include <pointer-analysis/andersen.h>
#include <util/config/config.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/base/prefix.h>
#include <util/irep/std_expr.h>
#include <util/message/message.h>
#include <iterator>
#include <memory>
#include <optional>
#include <unordered_map>
#include <unordered_set>

Include dependency graph for goto_k_induction.cpp:

Functions
bool	havoc_loop (goto_functionst &goto_functions, goto_functiont &goto_function, const loop_writest &w, bool continue_past_failed_assertions)
	Havocs what the loop of w writes and transforms it for the inductive step.
std::unordered_set< irep_idt, irep_id_hash >	unsettled_by_loops (goto_functionst &goto_functions)
	The locals and parameters some loop of their function havocs in the inductive step and may read the havoc of.
bool	goto_k_induction (goto_functionst &goto_functions, const namespacet &, 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).

havoc_loop()

bool havoc_loop	(	goto_functionst &	goto_functions,
		goto_functiont &	goto_function,
		const loop_writest &	w,
		bool	continue_past_failed_assertions )

Havocs what the loop of w writes and transforms it for the inductive step.

Returns false when a write through a pointer stays uncovered.

unsettled_by_loops()

std::unordered_set< irep_idt, irep_id_hash > unsettled_by_loops

(

goto_functionst &

goto_functions

)

The locals and parameters some loop of their function havocs in the inductive step and may read the havoc of.