diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:32 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 08:19:32 +0100 |
| commit | 0d471625d7613a72c0bb8519e0427f971b53b35f (patch) | |
| tree | 7478569a4118ff0cf851f8d491d628aa78454955 /common/Memdata.v | |
| parent | bc5b28ec16590c52da2772b1cc296247ccf528c1 (diff) | |
| parent | 3bdb983e0b21c8d45e85aff08278475396038f4f (diff) | |
| download | compcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.tar.gz compcert-kvx-0d471625d7613a72c0bb8519e0427f971b53b35f.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'common/Memdata.v')
| -rw-r--r-- | common/Memdata.v | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index 7144d72c..f3016efe 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -547,18 +547,26 @@ Proof. destruct v1; auto. Qed. -Lemma decode_val_type: +Lemma decode_val_rettype: forall chunk cl, - Val.has_type (decode_val chunk cl) (type_of_chunk chunk). + Val.has_rettype (decode_val chunk cl) (rettype_of_chunk chunk). Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. -Local Opaque Val.load_result. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). Qed. +Lemma decode_val_type: + forall chunk cl, + Val.has_type (decode_val chunk cl) (type_of_chunk chunk). +Proof. + intros. rewrite <- proj_rettype_of_chunk. + apply Val.has_proj_rettype. apply decode_val_rettype. +Qed. + Lemma encode_val_int8_signed_unsigned: forall v, encode_val Mint8signed v = encode_val Mint8unsigned v. Proof. @@ -607,11 +615,9 @@ Lemma decode_val_cast: | _ => True end. Proof. - unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. + intros. + assert (A: Val.has_rettype v (rettype_of_chunk chunk)) by apply decode_val_rettype. + destruct chunk; auto; simpl in A; destruct v; try contradiction; simpl; congruence. Qed. (** Pointers cannot be forged. *) |