1d0366ac5e
msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API
2016-02-02 15:57:28 +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
8fa63f07ba
aep-binding: finished infoflow
2015-09-16 11:41:01 +10:00
8451c17837
fixed decode with sorry
2015-09-15 12:02:26 +10: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
b46bc4e78d
infoflow: 2015 update (apart from C refinement)
2015-05-16 18:14:59 +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
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
50dda7708c
comment cleanup
2014-07-22 18:10:20 +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
Joel Beeren
Daniel Matichuk
Ramana Kumar
Gerwin Klein
David Greenaway
Thomas Sewell