diff options
Diffstat (limited to 'scheduling/RTLpathScheduler.v')
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index beab405f..6f90b455 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof] Require Import AST Linking Values Maps Globalenvs Smallstep Registers. Require Import Coqlib Maps Events Errors Op. Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl. - +Require RTLpathWFcheck. Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG)) (at level 200, A at level 100, B at level 200) @@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler". Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} := - match RTLpathLivegen.function_checker tfr tpm with + match RTLpathWFcheck.function_checker tfr tpm with | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed") | true => OK {| fn_RTL := tfr; fn_path := tpm |} end. Next Obligation. - apply function_checker_path_entry. auto. + apply RTLpathWFcheck.function_checker_path_entry. auto. Defined. Next Obligation. - apply function_checker_wellformed_path_map. auto. + apply RTLpathWFcheck.function_checker_wellformed_path_map. auto. Defined. Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit := |