Documentation

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

1 files changed, 9 insertions, 8 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 23faf785..d021a63c 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -26,16 +26,11 @@ Open Local Scope error_monad_scope.
   taken in the Csharpminor code can be mapped to Cminor local
   variable, since the latter do not reside in memory.  
 
-  Other tasks performed during the translation to Cminor:
-- Transformation of Csharpminor's standard set of operators and
-  trivial addressing modes to Cminor's processor-dependent operators
-  and addressing modes.  This is done using the optimizing Cminor
-  constructor functions provided in file [Cmconstr], therefore performing
-  instruction selection on the fly.
-- Insertion of truncation, zero- and sign-extension operations when
+  The other task performed during the translation to Cminor is the
+  insertion of truncation, zero- and sign-extension operations when
   assigning to a Csharpminor local variable of ``small'' type
   (e.g. [Mfloat32] or [Mint8signed]).  This is necessary to preserve
-  the ``normalize at assignment-time'' semantics of Csharpminor.
+  the ``normalize at assignment-time'' semantics of Clight and Csharpminor.
 *)
 
 (** Translation of constants. *)
@@ -62,6 +57,12 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
   | Mfloat64 => e
   end.
 
+(** When the translation of an expression is stored in memory,
+  the normalization performed by [make_cast] can be redundant
+  with that implicitly performed by the memory store.
+  [store_arg] detects this case and strips away the redundant
+  normalization. *)
+
 Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
   match e with
   | Eunop Ocast8signed e1 =>