interval_analysis.cpp File Reference

Interval Analysis – implements the functionality necessary for performing abstract interpretation over interval domain for goto programs. More...

#include "interval_analysis.h"
#include <util/find_symbols.h>
#include "ai.h"
#include "interval_domain.h"

Include dependency graph for interval_analysis.cpp:

Go to the source code of this file.

Functions
void	instrument_intervals (const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function)
	Instruments all "post-branch" instructions with assumptions about variable intervals. More...
void	interval_analysis (goto_modelt &goto_model)
	Initialises the abstract interpretation over interval domain and instruments instructions using interval assumptions. More...

Detailed Description

Interval Analysis – implements the functionality necessary for performing abstract interpretation over interval domain for goto programs.

The result of the analysis is an instrumented program.

Definition in file interval_analysis.cpp.

Function Documentation

instrument_intervals()

void instrument_intervals	(	const ait< interval_domaint > &	interval_analysis,
		goto_functionst::goto_functiont &	goto_function
	)

Instruments all "post-branch" instructions with assumptions about variable intervals.

For each such instruction, the function evaluates all variables referenced within the input goto_function as intervals, transforms these intervals into expressions and instruments the instruction with their conjunction. Example: interval [5,10] (for variable "x") translates into conjunction 5 <= x && x <= 10.

Parameters

	interval_analysis	Interval domain to be used for variable evaluation
[out]	goto_function	Goto function to be analysed and instrumented.

Definition at line 30 of file interval_analysis.cpp.

interval_analysis()

void interval_analysis

(

goto_modelt &

goto_model

)

Initialises the abstract interpretation over interval domain and instruments instructions using interval assumptions.

Parameters

[out]

goto_model

Input code as goto_model.

Definition at line 90 of file interval_analysis.cpp.