From 75fea20a8289e4441819b45d7ce750eda1b53ad1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 24 Mar 2014 09:10:35 +0000 Subject: Type-checking of builtin volatile write Mfloat32 was too strict, causing type errors after optimization. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2434 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 4 ++-- common/Events.v | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 6f35be0..29d1452 100644 --- a/common/AST.v +++ b/common/AST.v @@ -586,9 +586,9 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default + | EF_vstore chunk => mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk_use chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default diff --git a/common/Events.v b/common/Events.v index 8b6d25f..48cd91e 100644 --- a/common/Events.v +++ b/common/Events.v @@ -967,7 +967,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1022,7 +1022,7 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default). + (mksignature (type_of_chunk_use chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) -- cgit v1.2.3