From 362f2f36a44fa6ab4fe28264ed572d721adece70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 3 Jan 2014 17:09:54 +0000 Subject: 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 --- cfrontend/Ctypes.v | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'cfrontend') 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. -- cgit v1.2.3