diff options
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8529010c..28941e01 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -292,26 +292,26 @@ Definition iblock_step stack f sp rs m ib t s: Prop := of system calls performed during this transition. *) Inductive step: state -> trace -> state -> Prop := - | exec_iblock stack ib f sp pc rs m t s: - (fn_code f)!pc = Some ib -> - iblock_step stack f sp rs m ib.(entry) t s -> - step (State stack f sp pc rs m) t s - | exec_function_internal stack f args m m' stk: - Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - step (Callstate stack (Internal f) args m) - E0 (State stack + | exec_iblock stack ib f sp pc rs m t s + (PC: (fn_code f)!pc = Some ib) + (STEP: iblock_step stack f sp rs m ib.(entry) t s) + :step (State stack f sp pc rs m) t s + | exec_function_internal stack f args m m' stk + (ALLOC: Mem.alloc m 0 f.(fn_stacksize) = (m', stk)) + :step (Callstate stack (Internal f) args m) + E0 (State stack f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) m') - | exec_function_external stack ef args res t m m': - external_call ef ge args m t res m' -> - step (Callstate stack (External ef) args m) - t (Returnstate stack res m') - | exec_return stack res f sp pc rs vres m: - step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) - E0 (State stack f sp pc (rs#res <- vres) m) + | exec_function_external stack ef args res t m m' + (EXTCALL: external_call ef ge args m t res m') + :step (Callstate stack (External ef) args m) + t (Returnstate stack res m') + | exec_return stack res f sp pc rs vres m + :step (Returnstate (Stackframe res f sp pc rs :: stack) vres m) + E0 (State stack f sp pc (rs#res <- vres) m) . End RELSEM. |