bc73b112bd
l4v-sabre: change type of irq to be 10 word
2016-02-17 11:18:02 +11:00
1d0366ac5e
msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API
2016-02-02 15:57:28 +11:00
a1f23e5b28
arch_split: DRefine now builds
2016-01-25 18:42:27 +11:00
efb4c61816
archirq: Remove redundant invocation, renamed
...
arch_decode_interrupt_control.
2016-01-14 17:50:33 +11:00
457a55a831
add arch_tcb object to C, rename aep -> ntfn
2015-11-20 16:02:13 +11:00
0fb88ea01c
Merge branch 'master' into aep-merge
...
This commit should at least remove merge conflict markers, and the idea
is that at least refine, crefine, drefine, and infoflow (with sorrys)
build. Subsequent commits may be required to fix build issues that I
have not picked up.
2015-09-10 17:06:45 +10:00
d88a931ec7
history squashed patch for aep-binding
2015-09-02 15:43:39 +10:00
f6124669fc
2015 update for DRefine
2015-05-13 09:52:32 +02:00
0c004d2a93
Merge branch 'master' into 'isabelle-2014'.
...
Conflicts:
proof/drefine/Arch_DR.thy
proof/drefine/Finalise_DR.thy
proof/drefine/StateTranslation_D.thy
sys-init/DuplicateCaps_SI.thy
sys-init/Proof_SI.thy
tools/autocorres/tests/examples/SchorrWaite.thy
2014-09-23 14:31:33 +10:00
ea58753cd7
Merge branch 'cdl_page_map_cancel'
...
Merge in the setting of registers and the starting of threads in the system initialser.
2014-09-18 17:21:17 +10:00
cc71c3aadf
drefine: More updates for Isabelle 2014.
2014-09-18 11:04:47 +10:00
cf0d1abce6
Merge 'master' into 'isabelle-2014'.
...
Conflicts:
proof/crefine/Fastpath_C.thy
proof/drefine/KHeap_DR.thy
proof/infoflow/Noninterference.thy
spec/design/version
sys-init/DuplicateCaps_SI.thy
sys-init/InitTCB_SI.thy
sys-init/Proof_SI.thy
tools/asmrefine/SimplExport.thy
tools/autocorres/tests/examples/SchorrWaite.thy
2014-09-17 14:21:13 +10:00
47662af345
fix DSpecProofs
2014-09-09 15:57:52 +10:00
7167ea42ac
CapDL: Made IRQ Nodes a new object type, not a small CNode.
...
IRQ Nodes are now their own object type in capDL. This makes it much easier
to distinguish between "real" CNodes and IRQ Nodes.
Updated:
* the capDL refinement,
* the access proofs, and
* the system initialiser.
2014-09-09 14:07:50 +10:00
77dd554227
page_map_unmap_cancel : cdl spec changed and drefine fixed.
2014-09-05 14:48:22 +10:00
b3e2eb1f9d
ioapic: finished up to InfoFlowC
2014-08-28 15:56:26 +10:00
71e7dcc319
Fix Access, InfoFlow and DRefine.
2014-08-13 16:45:40 +10:00
1af1d2b67b
some of the global Isabelle2014 renames
...
option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel
2014-08-09 15:39:20 +10:00
9d9a325032
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 17:21:34 +02:00
84595f4233
release cleanup
2014-07-17 18:22:50 +02:00
2a03e81df4
Import release snapshot.
2014-07-14 21:32:44 +02:00
Gao Xin
Joel Beeren
Daniel Matichuk
Ramana Kumar
Gerwin Klein
David Greenaway
Andrew Boyton
Gao Xin
Thomas Sewell