summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-03-24 09:10:35 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-03-24 09:10:35 +0000
commit75fea20a8289e4441819b45d7ce750eda1b53ad1 (patch)
tree5f425efb2ee4b5f5fa263c067f5491e3ff8736c2
parentc7099a26a0b5fd13987454fbe9a56e2b2d711726 (diff)
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
-rw-r--r--common/AST.v4
-rw-r--r--common/Events.v4
2 files changed, 4 insertions, 4 deletions
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 *)