diff options
Diffstat (limited to 'scheduling/RTLpathScheduler.v')
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index 7804e454..31680256 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -156,7 +156,7 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let (tctetpm, dm) := untrusted_scheduler f in let (tcte, tpm) := tctetpm in let (tc, te) := tcte in - let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te (mkuntrustedanalysis None None) 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; OK (tf, dm). |