#
8173a37c |
|
13-Aug-2018 |
Mitchell Buckley <mitchell.buckley@data61.csiro.au> |
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
|
#
dac7a00e |
|
26-Aug-2018 |
Ilya Yanok <ilya.yanok@gmail.com> |
haskell: explicitly import Prelude hiding Word everywhere where it can clash with Word type defined by SEL4.
|
#
807a9792 |
|
15-Jul-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp haskell: use consistent ARMHYP_SMMU tag
|
#
d8d1ee01 |
|
28-Jun-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
haskell: unify arm and arm-hyp haskell files - both ARM and ARM_HYP haskell specs are now generated from the same set of files using cpp - callbacks and platform files are merged into one directory (ARM) - remove check-arm-hyp.py now that there are no ARM_HYP.lhs files
|
#
7b75ed2b |
|
06-Feb-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
haskell: make ARM resemble the output of ARM_HYP preprocessing The first step of merging the ARM hypervisor extensions into existing ARM is to make the current ARM look like the preprocessed output of ARM_HYP, which currently supports both platforms. NOTE: this requires updates to ARM Refine and CRefine due to shuffling around some constants (pteBits et al.). That is on its way.
|
#
6dad6a1c |
|
19-Jul-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
ExecSpec: arch-specific faults + VMFault -> ArchFault + ReservedIRQ * skeletons, adding new constructs (arch_tcb, arch_fault) * adjusting skeletons for ReserveIRQ + small change in haskell (ARM) Changes in: spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs:37:21 Due to "Defined but not used: ‘irq’" * arch-splitting faults in skeletons (ARM) * fix arch_tcb and asUser namespace issues in skeletons (ARM) * checking in current generated files tags: [VER-623][SELFOUR-413]
|
#
c92baf74 |
|
15-Jul-2016 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
Haskell: arch-specific faults + split VMFault -> ArchFault + ReservedIRQ Hypervisor extensions add extra fault types which are entirely arch-specific. While the concept of a VM fault exists on all platforms, these faults are also arch-specific. This change adds an ArchFault datatype and constructor to the generic Faults and Failures, and moves VMFault into ArchFault for the ARM platform. NOTE: fault indices have changed (generic goes before arch) as per the changes needed for SELFOUR-413, which is the seL4 C equivalent of this commit. * add arch faults and failures to SEL4.cabal * introduce and handle IRQReserved On ARM this does nothing, but on other platforms reserved IRQs are actually used. * split TCB into ArchTCB (userContext) * changing ArchFault to make haskell-translator to work tags: [VER-623][SELFOUR-413]
|
#
ebc7cbe5 |
|
23-May-2016 |
Japheth Lim <Japheth.Lim@nicta.com.au> |
haskell: move Haskell kernel into spec/
|