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/Csyntax.v | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'cfrontend/Csyntax.v')

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 979d0bca..f9463e65 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -29,8 +29,9 @@ Inductive type : Set :=
   | Tpointer: type -> type
   | Tarray: type -> Z -> type
   | Tfunction: typelist -> type -> type
-  | Tstruct: fieldlist -> type
-  | Tunion: fieldlist -> type
+  | Tstruct: ident -> fieldlist -> type
+  | Tunion: ident ->fieldlist -> type
+  | Tcomp_ptr: ident -> type
 
 with typelist : Set :=
   | Tnil: typelist
@@ -164,8 +165,9 @@ Fixpoint alignof (t: type) : Z :=
   | Tpointer _ => 4
   | Tarray t' n => alignof t'
   | Tfunction _ _ => 1
-  | Tstruct fld => alignof_fields fld
-  | Tunion fld => alignof_fields fld
+  | Tstruct _ fld => alignof_fields fld
+  | Tunion _ fld => alignof_fields fld
+  | Tcomp_ptr _ => 4
   end
 
 with alignof_fields (f: fieldlist) : Z :=
@@ -208,8 +210,9 @@ Fixpoint sizeof (t: type) : Z :=
   | Tpointer _ => 4
   | Tarray t' n => sizeof t' * Zmax 1 n
   | Tfunction _ _ => 1
-  | Tstruct fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
-  | Tunion fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tstruct _ fld => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
+  | Tunion _ fld => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tcomp_ptr _ => 4
   end
 
 with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z :=
@@ -285,8 +288,9 @@ Definition access_mode (ty: type) : mode :=
   | Tpointer _ => By_value Mint32
   | Tarray _ _ => By_reference
   | Tfunction _ _ => By_reference
-  | Tstruct fList => By_nothing
-  | Tunion fList => By_nothing
+  | Tstruct _ fList => By_nothing
+  | Tunion _ fList => By_nothing
+  | Tcomp_ptr _ => By_value Mint32
 end.
 
 (** Classification of arithmetic operations and comparisons *)
-- 
cgit