Loading...

Searching...

No Matches

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.

void interval_analysis (goto_modelt &goto_model)

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

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.