Interval Analysis. More...

#include <goto-programs/goto_functions.h>

Include dependency graph for interval_analysis.h:

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

Enumerations
enum class	INTERVAL_INSTRUMENTATION_MODE { NO_INSTRUMENTATION , ALL_INSTRUCTIONS_FULL , ALL_INSTRUCTIONS_LOCAL , GUARD_INSTRUCTIONS_FULL , GUARD_INSTRUCTIONS_LOCAL , LOOP_MODE }

Functions
void	interval_analysis (goto_functionst &goto_functions, const namespacet &ns, const optionst &options, bool continue_past_failed_assertions, const INTERVAL_INSTRUMENTATION_MODE instrument_mode=INTERVAL_INSTRUMENTATION_MODE::GUARD_INSTRUCTIONS_LOCAL)
void	instrument_loop_bounds_after_kind (goto_functionst &goto_functions, const namespacet &ns, const optionst &options, bool continue_past_failed_assertions)
	Post-k-induction loop-bounds instrumentation.

Detailed Description

Interval Analysis.

Enumeration Type Documentation

◆ INTERVAL_INSTRUMENTATION_MODE

enum class INTERVAL_INSTRUMENTATION_MODE

strong

Enumerator
NO_INSTRUMENTATION
ALL_INSTRUCTIONS_FULL
ALL_INSTRUCTIONS_LOCAL
GUARD_INSTRUCTIONS_FULL
GUARD_INSTRUCTIONS_LOCAL
LOOP_MODE

Function Documentation

◆ instrument_loop_bounds_after_kind()

void instrument_loop_bounds_after_kind	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		const optionst &	options,
		bool	continue_past_failed_assertions )

Post-k-induction loop-bounds instrumentation.

Re-runs interval analysis with inductive_step_instruction instructions (k-induction's nondet havocs and entry-condition assumes) treated as transparent no-ops, so the fixpoint at each loop head reflects the original program's dataflow. For every loop, inserts a single ASSUME(bounds) immediately before the loop's exit-test (the IF that k-induction's preamble runs into) — i.e. between the havoc'd assignments and the IF, so the bounds tighten the havoc'd values for the inductive step. The inserted ASSUME is marked inductive_step_instruction = true so base case and forward condition skip it.

Must run AFTER goto_k_induction(). Always runs the full ait fixpoint and per-loop scan; inserts no ASSUME for loops where every variable's bound simplifies to true (i.e. no useful tightening).

◆ interval_analysis()

void interval_analysis	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		const optionst &	options,
		bool	continue_past_failed_assertions,
		const INTERVAL_INSTRUMENTATION_MODE	instrument_mode = INTERVAL_INSTRUMENTATION_MODE::GUARD_INSTRUCTIONS_LOCAL )