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

x64: refine: update valid_irq_node

This commit is contained in:
Joel Beeren 2017-03-31 16:58:31 +11:00
parent 71118f3e40
commit 1768779b90
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/refine/X64/Invariants_H.thy
View File

@ -1009,7 +1009,7 @@ definition
valid_irq_node' :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"valid_irq_node' x \<equiv>
\<lambda>s. is_aligned x 12 \<and> (\<forall>irq :: irq. real_cte_at' (x + 16 * (ucast irq)) s)"
\<lambda>s. is_aligned x 12 \<and> (\<forall>irq :: irq. real_cte_at' (x + 32 * (ucast irq)) s)"
definition
valid_refs' :: "machine_word set \<Rightarrow> cte_heap \<Rightarrow> bool"