diff options
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/common/Events.v b/common/Events.v index 24c03dc..cf57650 100644 --- a/common/Events.v +++ b/common/Events.v @@ -764,7 +764,7 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk))). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -826,7 +826,7 @@ Qed. Lemma volatile_load_global_ok: forall chunk id ofs, extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk))). + (mksignature nil (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -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). + (mksignature (Tint :: type_of_chunk 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). + (mksignature (type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1070,7 +1070,7 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint)). + (mksignature (Tint :: nil) (Some Tint) cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1145,7 +1145,7 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None). + (mksignature (Tint :: nil) None cc_default). Proof. constructor; intros. (* well typed *) @@ -1241,7 +1241,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). + extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. (* return type *) @@ -1337,7 +1337,7 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None). + extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1381,7 +1381,7 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). + extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1433,7 +1433,7 @@ Axiom external_functions_properties: Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). (** ** Combined semantics of external calls *) |