Merge pull request #2781 from smowton/smowton/docs/fi-analysis

Briefly document flow-insensitive analysis

Author: Daniel Kroening

src/analyses/README.md

@@ -18,7 +18,17 @@ This is obsolete.
 
 \subsection analyses-flow-insensitive-analysis Flow-insensitive analysis (flow_insensitive_analysist)
 
-To be documented.
+Framework for flow-insensitive analyses. Maintains a single global abstract
+value which instructions are invited to transform in turn. Unsound (terminates
+too early) if
+(a) there are two or more instructions that incrementally reach a fixed point,
+for example by walking a chain of pointers and updating a points-to set, but
+(b) those instructions are separated by instructions that don't update the
+abstract value (for example, SKIP instructions). Therefore, not recommended for
+new code.
+
+Only current user in-tree is \ref value_set_analysis_fit and its close
+relatives, \ref value_set_analysis_fivrt and \ref value_set_analysis_fivrnst
 
 \section analyses-specific-analyses Specific analyses:
 

src/analyses/flow_insensitive_analysis.h

@@ -9,6 +9,17 @@ Author: Daniel Kroening, [email protected]
 
 /// \file
 /// Flow Insensitive Static Analysis
+///
+/// A framework for flow-insensitive analyses. Maintains a single global
+/// abstract value (an instance of \ref flow_insensitive_abstract_domain_baset,
+/// "the domain,") which instructions are invited to transform in turn.
+///
+/// Note this is unsound if used naively, because it follows the control-flow
+/// graph and terminates when an instruction makes no change to the domain and
+/// that instruction's successors have already been visited. Therefore a domain
+/// that relies upon every reachable instruction being re-visited upon the
+/// domain being updated must ensure that itself, for example by maintaining
+/// a map from locations to the latest version of the domain witnessed.
 
 #ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
 #define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H