diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 18:00:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 18:00:14 +0200 |
| commit | 60e4ad85c6cd433c9e28c9e407a957ca3a302c22 (patch) | |
| tree | f2681ea08e2948baa2df6b47932c23c575ad4d43 /backend/CSE3proof.v | |
| parent | 8cf7fae8c94f5d394712428d3c2f627ea7f2d279 (diff) | |
| download | compcert-kvx-60e4ad85c6cd433c9e28c9e407a957ca3a302c22.tar.gz compcert-kvx-60e4ad85c6cd433c9e28c9e407a957ca3a302c22.zip | |
CSE3: better builtin handling
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 19fb20be..53872e62 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -224,7 +224,6 @@ Proof. eapply function_ptr_translated; eauto. Qed. -Check sem_rel_b. Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := | match_stackframes_nil: forall sg, sg.(sig_res) = Tint -> @@ -428,8 +427,8 @@ Ltac IND_STEP := destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; simpl in *; intuition; - eapply rel_ge; eauto with cse3; - idtac mpc mpc' fn minstr + eapply rel_ge; eauto with cse3 (* ; for printing + idtac mpc mpc' fn minstr *) end. Lemma if_same : forall {T : Type} (b : bool) (x : T), @@ -753,6 +752,9 @@ Proof. + econstructor; eauto. * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. * IND_STEP. + apply kill_builtin_res_sound; eauto with cse3. + eapply external_call_sound; eauto with cse3. + - (* Icond *) econstructor. split. + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. |