Add overview of constant propagator

Author: smowton

src/analyses/README.md

@@ -30,9 +30,12 @@ To be documented.
 
 To be documented.
 
-\subsection analyses-constant-propagation Constant propagation (constant_propagator_ait)
+\subsection analyses-constant-propagation Constant propagation (\ref constant_propagator_ait)
 
-To be documented.
+A simple, unsound constant propagator. Replaces RHS symbol expressions (variable
+reads) with their values when they appear to have a unique value at a particular
+program point. Unsound with respect to pointer operations on the left-hand side
+of assignments.
 
 \subsection analyses-taint Taint analysis (custom_bitvector_analysist)
 

src/analyses/constant_propagator.h

@@ -8,6 +8,16 @@ Author: Peter Schrammel
 
 /// \file
 /// Constant propagation
+///
+/// A simple, unsound constant propagator. Assignments to symbols (local and
+/// global variables) are tracked, and propagated if a unique value is found
+/// at a given use site. Function calls are accounted for (they are assumed to
+/// overwrite all address-taken variables; see \ref dirtyt), but assignments
+/// through pointers are not (they are assumed to have no effect).
+///
+/// Can be restricted to operate over only particular symbols by passing a
+/// predicate to a \ref constant_propagator_ait constructor, in which case this
+/// can be rendered sound by restricting it to non-address-taken variables.
 
 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H