diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 16:01:12 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-18 16:01:12 +0200 |
commit | c85b6a585073f3fc7c8e34fbd78c613bf619cbeb (patch) | |
tree | 6eda17523dd996fb0f6ccc426773ceb2b516a235 | |
parent | 7fb3cf8821f0fbb89cab74425c6c84f85e913b08 (diff) | |
download | compcert-c85b6a585073f3fc7c8e34fbd78c613bf619cbeb.tar.gz compcert-c85b6a585073f3fc7c8e34fbd78c613bf619cbeb.zip |
Missing case in ValueDomain.pincl, causing incompleteness.
-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. |