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

x64: abstract: minor tweak to throws in arch_decode_irq_control_invocation

This commit is contained in:
Joel Beeren 2017-04-11 18:37:30 +10:00
parent 3935de8050
commit a9e8518c1d
2 changed files with 4 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
proof/invariant-abstract/X64/ArchInterrupt_AI.thy
View File

@ -14,7 +14,6 @@ begin
context Arch begin global_naming X64
thm irq_control_inv_valid.simps arch_decode_irq_control_invocation_def
primrec arch_irq_control_inv_valid_real :: "arch_irq_control_invocation \<Rightarrow> 'a::state_ext state \<Rightarrow> bool"
where
"arch_irq_control_inv_valid_real (IssueIRQHandlerIOAPIC irq dest_slot src_slot

10
spec/abstract/X64/ArchDecode_A.thy
View File

@ -67,18 +67,16 @@ definition
in doE
whenE (x > ucast maxIRQ) $ throwError (RangeError 0 (ucast maxIRQ));
dest_slot \<leftarrow> lookup_target_slot cnode (data_to_cptr index) (unat depth);
ensure_empty dest_slot;
irq_active \<leftarrow> liftE $ is_irq_active irqv;
whenE irq_active $ throwError RevokeFirst;
dest_slot \<leftarrow> lookup_target_slot cnode (data_to_cptr index) (unat depth);
ensure_empty dest_slot;
(* Following should be wrapped in to a funcion like what c did
since it is pc99 related, problem is where to put this function*)
whenE (ioapic > numIOAPICs - 1) $ throwError (RangeError 0 numIOAPICs);
whenE (pin > ioapicIRQLines - 1) $ throwError (RangeError 0 ioapicIRQLines);
whenE (ioapic > numIOAPICs - 1) $ throwError (RangeError 0 (numIOAPICs-1));
whenE (pin > ioapicIRQLines - 1) $ throwError (RangeError 0 (ioapicIRQLines-1));
whenE (level > 1) $ throwError (RangeError 0 1);
whenE (polarity > 1) $ throwError (RangeError 0 1);