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 /backend/ValueDomain.v | |
| parent | 7fb3cf8821f0fbb89cab74425c6c84f85e913b08 (diff) | |
| download | compcert-kvx-c85b6a585073f3fc7c8e34fbd78c613bf619cbeb.tar.gz compcert-kvx-c85b6a585073f3fc7c8e34fbd78c613bf619cbeb.zip | |
Missing case in ValueDomain.pincl, causing incompleteness.
Diffstat (limited to 'backend/ValueDomain.v')
| -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. |