diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 20:07:50 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 20:07:50 +0100 |
| commit | 6f71a2a369d07a8e812fb3893f30be528b28d3ee (patch) | |
| tree | d12323efa719226e072abd955a7302eaa3b546c7 /scheduling | |
| parent | ef67224a0ec3ef67db98198008e7f9d5bfc79ca8 (diff) | |
| download | compcert-kvx-6f71a2a369d07a8e812fb3893f30be528b28d3ee.tar.gz compcert-kvx-6f71a2a369d07a8e812fb3893f30be528b28d3ee.zip | |
Adding fp init expansions
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index 79129872..31680256 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -158,7 +158,7 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let (tc, te) := tcte in let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do tf <- proj1_sig (function_builder tfr tpm); - (*do tt <- function_equiv_checker dm f tf; *) + do tt <- function_equiv_checker dm f tf; OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -171,7 +171,7 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path tf) pc2) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) . -Proof. Admitted. (* +Proof. intros VERIF. unfold verified_scheduler in VERIF. explore. Local Hint Resolve function_equiv_checker_entrypoint function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 @@ -180,7 +180,7 @@ Proof. Admitted. (* apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition. - Qed. *) +Qed. Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; |