Comments

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 0 deletions

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 3085f96..f1e3d41 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -39,6 +39,13 @@ Require Import Linear.
 
 (** * Tracking the flow of single-precision floats *)
 
+(** At each program point, we infer a set of machine registers
+  that are guaranteed to contain single-precision floats.
+  The inference is a simple forward dataflow analysis, iterating on the 
+  list of instructions until a fixpoint is reached.  The result of
+  the analysis is a map from labels to sets of machine registers
+  containing single-precision floats.  *)
+
 Module OrderedMreg := OrderedIndexed(IndexedMreg).
 Module Regset := FSetAVL.Make(OrderedMreg).