diff options
Diffstat (limited to 'ia32/ConstpropOpproof.v')
| -rw-r--r-- | ia32/ConstpropOpproof.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index d792d8a5..b6c3cdc3 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -44,9 +44,10 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | Unknown => True | I p => v = Vint p | F p => v = Vfloat p + | L p => v = Vlong p | G symb ofs => v = symbol_address ge symb ofs | S ofs => v = Val.add sp (Vint ofs) - | _ => False + | Novalue => False end. Inductive val_list_match_approx: list approx -> list val -> Prop := @@ -64,6 +65,8 @@ Ltac SimplVMA := simpl in H; (try subst v); SimplVMA | H: (val_match_approx (F _) ?v) |- _ => simpl in H; (try subst v); SimplVMA + | H: (val_match_approx (L _) ?v) |- _ => + simpl in H; (try subst v); SimplVMA | H: (val_match_approx (G _ _) ?v) |- _ => simpl in H; (try subst v); SimplVMA | H: (val_match_approx (S _) ?v) |- _ => @@ -156,6 +159,8 @@ Proof. destruct (Int.ltu n2 Int.iwordsize); simpl; auto. destruct (Int.ltu n Int.iwordsize); simpl; auto. destruct (Int.ltu n Int.iwordsize); simpl; auto. + destruct (Int.ltu n Int.iwordsize); + destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize); simpl; auto. eapply eval_static_addressing_correct; eauto. unfold eval_static_intoffloat. destruct (Float.intoffloat n1) eqn:?; simpl in H0; inv H0. |