diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:15:48 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:15:48 +0100 |
| commit | b2c91fd80fc88f4583ceee56243c5845cb1a93ef (patch) | |
| tree | 8adc62e43706dc2d6e91510b2eb6e8d60a7ba33f /backend/CSE3proof.v | |
| parent | 54544caeeb95437741a543a50ed22b8e5549691f (diff) | |
| download | compcert-kvx-b2c91fd80fc88f4583ceee56243c5845cb1a93ef.tar.gz compcert-kvx-b2c91fd80fc88f4583ceee56243c5845cb1a93ef.zip | |
no more 'admit' in CSE3
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 888aa55e..a6de5a5f 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -678,9 +678,11 @@ Proof. - (* Istore *) exists (State ts tf sp pc' rs m'). split. - + eapply exec_Istore; try eassumption. + + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. * TR_AT. reflexivity. - * admit. + * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved. + assumption. + econstructor; eauto. IND_STEP. apply store_sound with (a0:=a) (m0:=m); eauto with cse3. |