From be43363d309cea62731e04ad10dddf3ecafcacd1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 11 Sep 2006 16:03:02 +0000
Subject: Revu traitement des structures et unions recursives.  Dans Cshmgen,
 meilleure compilation de exit_if_false.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cshmgen.v | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'cfrontend/Cshmgen.v')

diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5585416b..aaec07d8 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -41,8 +41,9 @@ Definition var_kind_of_type (ty: type): option var_kind :=
   | Tpointer _ => Some(Vscalar Mint32)
   | Tarray _ _ => Some(Varray (Csyntax.sizeof ty))
   | Tfunction _ _ => None
-  | Tstruct fList => Some(Varray (Csyntax.sizeof ty))
-  | Tunion fList => Some(Varray (Csyntax.sizeof ty))
+  | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty))
+  | Tunion _ fList => Some(Varray (Csyntax.sizeof ty))
+  | Tcomp_ptr _ => Some(Vscalar Mint32)
 end.
   
 (** ** Csharpminor constructors *)
@@ -359,13 +360,13 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
       Some(make_intconst (Int.repr (Csyntax.sizeof ty)))
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
-      | Tstruct fld =>
+      | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
           make_load
             (make_binop Oadd tb (make_intconst (Int.repr ofs)))
             ty
-      | Tunion fld =>
+      | Tunion _ fld =>
           do tb <- transl_lvalue b;
           make_load tb ty
       | _ => None
@@ -389,11 +390,11 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
       make_add tb (typeof b) tc (typeof c)
   | Expr (Csyntax.Efield b i) ty => 
       match typeof b with
-      | Tstruct fld =>
+      | Tstruct _ fld =>
           do tb <- transl_lvalue b;
           do ofs <- field_offset i fld;
           Some (make_binop Oadd tb (make_intconst (Int.repr ofs)))
-      | Tunion fld =>
+      | Tunion _ fld =>
           transl_lvalue b
       | _ => None
       end
@@ -430,9 +431,9 @@ Definition is_variable (e: Csyntax.expr) : option ident :=
 Definition exit_if_false (e: Csyntax.expr) : option stmt :=
   do te <- transl_expr e;
   Some(Sifthenelse
-        (make_notbool te (typeof e))
-        (Sexit 0%nat)
-        Sskip).
+        (make_boolean te (typeof e))
+        Sskip
+        (Sexit 0%nat)).
 
 (* [transl_statement nbrk ncnt s] returns a Csharpminor statement
    that performs the same computations as the CabsCoq statement [s].
-- 
cgit