diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 06:13:05 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 06:13:05 +0100 |
| commit | a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08 (patch) | |
| tree | 5f22972f5e9c74999dab5405757aae9f9631a258 /backend/CSE2proof.v | |
| parent | 93bf7e0925b1c11e1874ae5f651970db2bd9823d (diff) | |
| download | compcert-kvx-a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08.tar.gz compcert-kvx-a398b5750ceeeab90a44b2e1d34fe6d5ff8b1f08.zip | |
with indexed/indexed alias analysis for x86
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index cd9f5f46..e65d9194 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -951,6 +951,7 @@ Definition fmap_sem' := fmap_sem fundef unit ge. Definition subst_arg_ok' := subst_arg_ok fundef unit ge. Definition subst_args_ok' := subst_args_ok fundef unit ge. Definition kill_mem_sound' := kill_mem_sound fundef unit ge. +Definition kill_store_sound' := kill_store_sound fundef unit ge. Lemma sem_rel_b_ge: forall rb1 rb2 : RB.t, @@ -1260,8 +1261,7 @@ Proof. rewrite H. reflexivity. } - apply (kill_store_sound' sp m). - assumption. + eapply (kill_store_sound' sp m); eassumption. (* call *) - econstructor; split. |