Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


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

1 files changed, 14 insertions, 1 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index 243f6dd..6801013 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -178,6 +178,15 @@ Definition add_load (n: numbering) (rd: reg)
   let (n1, vs) := valnum_regs n rs in
   add_rhs n1 rd (Load chunk addr vs).
 
+(** [add_unknown n rd] returns a numbering where [rd] is mapped to a
+   fresh value number, and no equations are added.  This is useful
+   to model instructions with unpredictable results such as [Ialloc]. *)
+
+Definition add_unknown (n: numbering) (rd: reg) :=
+  mknumbering (Psucc n.(num_next))
+              n.(num_eqs)
+              (PTree.set rd n.(num_next) n.(num_reg)).
+
 (** [kill_load n] removes all equations involving memory loads.
   It is used to reflect the effect of a memory store, which can
   potentially invalidate all such equations. *)
@@ -328,6 +337,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
           kill_loads before
       | Icall sig ros args res s =>
           empty_numbering
+      | Ialloc arg res s =>
+          add_unknown before res
       | Icond cond args ifso ifnot =>
           before
       | Ireturn optarg =>
@@ -415,6 +426,8 @@ Definition transf_function (f: function) : function :=
         f.(fn_nextpc)
         (transf_code_wf f approxs f.(fn_code_wf)).
 
+Definition transf_fundef := AST.transf_fundef transf_function.
+
 Definition transf_program (p: program) : program :=
-  transform_program transf_function p.
+  transform_program transf_fundef p.