diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-11 16:03:02 +0000 |
| commit | be43363d309cea62731e04ad10dddf3ecafcacd1 (patch) | |
| tree | f66c346d51df74d6b6ee34f654178a44250a33c8 /cfrontend/Csyntax.v | |
| parent | 5e8237152cad0cf08d3eea0d5de8cd8bc499df69 (diff) | |
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
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 979d0bc..f9463e6 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 *) |