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

arm_hyp crefine: fixes for idle_tcb'/valid_idle' change 

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2021-04-14 14:21:26 +10:00 committed by Miki Tanaka
parent 376cc707b6
commit fe2329dbb9
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/ARM_HYP/Interrupt_C.thy
View File

@ -52,7 +52,7 @@ lemma cte_at_irq_node':
"invs' s \<Longrightarrow>
cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 10 word)) s"
by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
cte_level_bits_def real_cte_at')
cte_level_bits_def real_cte_at' cteSizeBits_def shiftl_t2n)
lemma invokeIRQHandler_SetIRQHandler_ccorres:
"ccorres dc xfdc

2
proof/crefine/ARM_HYP/Retype_C.thy
View File

@ -8514,7 +8514,7 @@ shows "ccorres dc xfdc
apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def
dest!:invs_valid_idle' elim!: obj_atE')
apply (drule(1) pspace_no_overlapD')
apply (erule_tac x = "ksIdleThread s" in in_empty_interE[rotated])
apply (rule_tac x = "ksIdleThread s" in in_empty_interE[rotated], simp)
prefer 2
apply (simp add:Int_ac)
subgoal by (clarsimp simp: blah)