diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 11:12:00 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 11:12:00 +0100 |
| commit | 085e4f45ebf81b7734efa70f018928ac49703f47 (patch) | |
| tree | cec7f94e308c3cbe470c3a0dc930be2d7394fee7 /backend/CSE3proof.v | |
| parent | 7bc6519d4f72f2b7f6cd26f177dec12e35a4b47f (diff) | |
| download | compcert-kvx-085e4f45ebf81b7734efa70f018928ac49703f47.tar.gz compcert-kvx-085e4f45ebf81b7734efa70f018928ac49703f47.zip | |
inductive
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index bdf5ecd7..f63636ce 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -142,6 +142,19 @@ Proof. exists x. assumption. Qed. +Lemma transf_function_invariants_inductive: + forall f tf tenv, transf_function f = OK tf -> + type_function f = OK tenv -> + check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f)))) + f tenv (fst (preanalysis tenv f)) = true. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + replace x with tenv in * by congruence. + clear x. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness; trivial; discriminate. +Qed. Lemma find_function_translated: forall ros rs fd, |