Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

1 files changed, 5 insertions, 14 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index dab8fc31..4347c334 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -375,23 +375,14 @@ Definition analyze (f: RTL.function): PMap.t numbering :=
 
 (** * Code transformation *)
 
-(** Some operations are so cheap to compute that it is generally not
-  worth reusing their results.  These operations are detected by the
-  function below. *)
-
-Definition is_trivial_op (op: operation) : bool :=
-  match op with
-  | Omove => true
-  | Ointconst _ => true
-  | Oaddrsymbol _ _ => true
-  | Oaddrstack _ => true
-  | _ => false
-  end.
-
 (** The code transformation is performed instruction by instruction.
   [Iload] instructions and non-trivial [Iop] instructions are turned
   into move instructions if their result is already available in a
-  register, as indicated by the numbering inferred at that program point. *)
+  register, as indicated by the numbering inferred at that program point.
+
+  Some operations are so cheap to compute that it is generally not
+  worth reusing their results.  These operations are detected by the
+  function [is_trivial_op] in module [Op]. *)
 
 Definition transf_instr (n: numbering) (instr: instruction) :=
   match instr with