diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:45:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 13:45:14 +0200 |
| commit | 5cc18b7860630f822ada1e56ae73c6d96b372361 (patch) | |
| tree | 1e6877d6d84f2a121a5b8aa74b781bd54060dd16 /mppa_k1c | |
| parent | 819e0e55f945923adc6e8cfccb2e7a9b44a814ac (diff) | |
| download | compcert-kvx-5cc18b7860630f822ada1e56ae73c6d96b372361.tar.gz compcert-kvx-5cc18b7860630f822ada1e56ae73c6d96b372361.zip | |
some more simplifications
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 1 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index ed2006b0..811a8ab1 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -276,6 +276,7 @@ Nondetfunction orlimm (n1: int64) (e2: expr) := match e2 with | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2) | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil) + | Eop Onotl (t2:::Enil) => Eop (Oornlimm n1) (t2:::Enil) | _ => Eop (Oorlimm n1) (e2:::Enil) end. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 0700ac4d..3fa35331 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -439,6 +439,7 @@ Proof. destruct (orlimm_match a); InvEval; subst. - econstructor; split. apply eval_longconst. simpl. rewrite Int64.or_commut; auto. - TrivialExists. simpl. rewrite Val.orl_assoc. rewrite Int64.or_commut; auto. +- InvEval. TrivialExists. - TrivialExists. Qed. |