diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 15:18:50 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-10 15:18:50 +0200 |
| commit | 67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d (patch) | |
| tree | 52f7fc7d4cde6c7144b789d4df730b831753337a /mppa_k1c/Asmgenproof.v | |
| parent | e6fd7a6abcebee211acf1ef95e0779d7c8aa1325 (diff) | |
| download | compcert-kvx-67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d.tar.gz compcert-kvx-67a5ffd5f8a1f2f95dc480daee9b5d927c768a2d.zip | |
MPPA - bunch of ops added : lowlong, and, or, shr..
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index a7a41f18..c8a89ef3 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -307,8 +307,14 @@ Opaque Int.eq. - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. (* Oaddimm32 *) - apply opimm32_label; intros; exact I. +(* Oandimm32 *) +- apply opimm32_label; intros; exact I. (* Oaddimm64 *) - apply opimm64_label; intros; exact I. +(* Oandimm64 *) +- apply opimm64_label; intros; exact I. +(* Oorimm64 *) +- apply opimm64_label; intros; exact I. Qed. (* |