diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:44:56 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:44:56 +0200 |
| commit | 98206d8c97cf9ecdff8d892ecafb9a9fa8455f74 (patch) | |
| tree | 5d05d5a2907de5152c4566c1a172734c6a8ab651 /mppa_k1c/ConstpropOpproof.v | |
| parent | 9f256a4ad30c93749e6c1192a84f996feac3b023 (diff) | |
| download | compcert-kvx-98206d8c97cf9ecdff8d892ecafb9a9fa8455f74.tar.gz compcert-kvx-98206d8c97cf9ecdff8d892ecafb9a9fa8455f74.zip | |
fix slow globals etc.
Diffstat (limited to 'mppa_k1c/ConstpropOpproof.v')
| -rw-r--r-- | mppa_k1c/ConstpropOpproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index b6c73281..ae11a220 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -730,7 +730,7 @@ Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- destruct (Archi.pic_code tt). +- destruct (orb _ _). + exists (Val.offset_ptr e#r1 n); auto. + simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. inv H0; simpl; auto. |