diff options
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. |