Briefly document flow-insensitive analysis

Author: smowton

src/analyses/README.md

@@ -18,7 +18,16 @@ 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 domain 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
+domain (for example, SKIP instructions) unless the domain carefully avoids this
+fate. 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,16 @@ Author: Daniel Kroening, [email protected]
 
 /// \file
 /// Flow Insensitive Static Analysis
+///
+/// A framework for flow-insensitive analyses. Maintains a single global 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