Merge pull request #2791 from xbauch/develop

Briefly document interval analysis

Author: petr-bauch

src/analyses/README.md

@@ -139,6 +139,9 @@ To be documented.
 
 To be documented.
 
-\subsection analyses-interval-analysist Integer interval analysis (interval_analysist) -- both an analysis and a transformation
+\subsection analyses-interval-analysis Integer interval analysis -- both an analysis and a transformation
 
-To be documented.
+\ref interval_analysis interprets instructions of the input \ref goto_modelt
+over the \ref interval_domaint, evaluates variables for each program location
+(as intervals) and instruments the program with assumptions representing the
+over-approximation of variable values.

src/analyses/interval_analysis.cpp

@@ -7,14 +7,25 @@ Author: Daniel Kroening, [email protected]
 \*******************************************************************/
 
 /// \file
-/// Interval Analysis
+/// 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.
 
 #include "interval_analysis.h"
 
 #include <util/find_symbols.h>
 
 #include "interval_domain.h"
 
+/// 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.
+/// \param interval_analysis Interval domain to be used for variable evaluation.
+/// \param goto_function [out] Goto function to be analysed and instrumented.
 void instrument_intervals(
   const ait<interval_domaint> &interval_analysis,
   goto_functionst::goto_functiont &goto_function)
@@ -76,6 +87,9 @@ void instrument_intervals(
   }
 }
 
+/// Initialises the abstract interpretation over interval domain and
+/// instruments instructions using interval assumptions.
+/// \param goto_model [out] Input code as goto_model.
 void interval_analysis(goto_modelt &goto_model)
 {
   ait<interval_domaint> interval_analysis;