diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 16:52:19 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-06 16:52:19 +0100 |
| commit | 0b402973b88e85662dda8807b1839e1e5b0a56df (patch) | |
| tree | d99e10c3bad53aa3194d56823a141603e0b91d15 /scheduling | |
| parent | eb35c3000530e379dcd79e82f001a400be8b28e9 (diff) | |
| parent | 9882b3427b9dfc7e8f2de3402773fb3a1a49f14a (diff) | |
| download | compcert-kvx-0b402973b88e85662dda8807b1839e1e5b0a56df.tar.gz compcert-kvx-0b402973b88e85662dda8807b1839e1e5b0a56df.zip | |
Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 2 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 12aba56b..e21d7cd1 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -819,7 +819,7 @@ Proof. rewrite <- X, sok_local_set_sreg. intuition eauto. - destruct REF; intuition eauto. - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. - Qed. +Qed. Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index c2183937..6dc00227 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -298,11 +298,11 @@ let rec do_schedule code pm = function let new_code = apply_schedule code' sb schedule in begin (*debug_flag := true;*) + if code != code_exp then ( debug "Old Code: "; print_code code; - debug "Exp Code: "; print_code code_exp; - (*debug_flag := false; *) - debug "\nSchedule to apply: "; print_arrayp schedule; - debug "\nNew Code: "; print_code new_code; + debug "Exp Code: "; print_code code_exp); + (*debug "\nSchedule to apply: "; print_arrayp schedule;*) + (*debug "\nNew Code: "; print_code new_code;*) debug "\n"; do_schedule new_code pm lsb end |