diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/ValueDomain.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 3d0196d3..0de17745 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -301,6 +301,7 @@ Definition pincl (p q: aptr) : bool := | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true | Stk ofs1, Stk ofs2 => Int.eq_dec ofs1 ofs2 | Stk ofs1, Stack => true + | Stack, Stack => true | _, Ptop => true | _, _ => false end. @@ -311,6 +312,14 @@ Proof. InvBooleans; subst; auto with va. Qed. +Lemma pincl_ge_2: forall p q, pge p q -> pincl q p = true. +Proof. + destruct 1; simpl; auto. +- destruct p; auto. +- destruct p; simpl; auto; rewrite ! proj_sumbool_is_true; auto. +- rewrite ! proj_sumbool_is_true; auto. +Qed. + Lemma pincl_sound: forall b ofs p q, pincl p q = true -> pmatch b ofs p -> pmatch b ofs q. |