diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
| commit | 362f2f36a44fa6ab4fe28264ed572d721adece70 (patch) | |
| tree | 2f1b23f88fe906ae554e963acbcde09c54b1b5fb /cfrontend | |
| parent | 089c6c6dc139a0c32f8566d028702d39d0748077 (diff) | |
Introduce and use the platform-specific Archi module giving:
- endianness
- alignment constraints for 8-byte types
(which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Ctypes.v | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index ec4780e..5cd032d 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -18,6 +18,7 @@ Require Import Coqlib. Require Import AST. Require Import Errors. +Require Archi. (** * Syntax of types *) @@ -172,9 +173,9 @@ Fixpoint alignof (t: type) : Z := | Tint I16 _ _ => 2 | Tint I32 _ _ => 4 | Tint IBool _ _ => 1 - | Tlong _ _ => 8 + | Tlong _ _ => Archi.align_int64 | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 + | Tfloat F64 _ => Archi.align_float64 | Tpointer _ _ => 4 | Tarray t' _ _ => alignof t' | Tfunction _ _ _ => 1 @@ -214,10 +215,14 @@ Proof. induction t; apply X; simpl; auto. exists 0%nat; auto. destruct i. - exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto. - exists 0%nat; auto. exists 3%nat; auto. + exists 0%nat; auto. + exists 1%nat; auto. + exists 2%nat; auto. + exists 0%nat; auto. + (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). destruct f. - exists 2%nat; auto. exists 3%nat; auto. + exists 2%nat; auto. + (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). exists 2%nat; auto. exists 0%nat; auto. exists 2%nat; auto. @@ -311,8 +316,8 @@ Local Transparent alignof. induction t; simpl; intros. - apply Zdivide_refl. - rewrite H. destruct i; apply Zdivide_refl. -- rewrite H; apply Zdivide_refl. -- rewrite H. destruct f; apply Zdivide_refl. +- rewrite H. exists (8 / Archi.align_int64); reflexivity. +- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. - rewrite H; apply Zdivide_refl. - destruct H. rewrite H. apply Z.divide_mul_l; auto. - apply Zdivide_refl. |