adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

crefine: ARM verification support for "Disable active VCPU when switching to the idle thread"

This commit is contained in:
Rafal Kolanski 2017-03-06 15:56:10 +11:00
parent a94f5d0e69
commit 5ece85b8d2
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/crefine/Schedule_C.thy
View File

@ -158,6 +158,7 @@ lemma Arch_switchToIdleThread_ccorres:
"ccorres dc xfdc (valid_pspace' and valid_arch_state') UNIV []
Arch.switchToIdleThread (Call Arch_switchToIdleThread_'proc)"
apply (cinit simp: ARM_H.switchToIdleThread_def)
apply ccorres_rewrite
by (rule ccorres_return_Skip, clarsimp)
(* FIXME: move *)