diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
commit | c0bc146622528e3d52534909f5ae5cd2e375da8f (patch) | |
tree | 52c5f163a82b04d7ad56055b4bd5e852be168ae4 /cfrontend/Cminorgen.v | |
parent | adc9e990a0c338cef57ff1bd9717adcc781f283c (diff) | |
download | compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.tar.gz compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.zip |
Documentation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r-- | cfrontend/Cminorgen.v | 17 |
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 => |