diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:00:06 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:00:06 +0100 |
| commit | 71a3e11b500713b53f13fe64b87ebeb1c9c6e312 (patch) | |
| tree | 4508aefe3368787ee1c0ab47a8924ef2fe1bf398 /backend/CSE3proof.v | |
| parent | 8b9a4cb340bc135da9907c7d313caa11d078cb16 (diff) | |
| download | compcert-kvx-71a3e11b500713b53f13fe64b87ebeb1c9c6e312.tar.gz compcert-kvx-71a3e11b500713b53f13fe64b87ebeb1c9c6e312.zip | |
Ijumptable
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 8a49fe87..cd129cb2 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -652,9 +652,10 @@ Proof. - (* Ijumptable *) econstructor. split. - + eapply exec_Ijumptable; try eassumption. - erewrite transf_function_at by eauto. simpl. - admit. + + eapply exec_Ijumptable with (arg := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. + assumption. + econstructor; eauto. assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption). IND_STEP. |