#
a45adef6 |
|
31-Oct-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
all: remove theory import path references In Isabelle2020, when isabelle jedit is started without a session context, e.g. `isabelle jedit -l ASpec`, theory imports with path references cause the isabelle process to hang. Since sessions now declare directories, Isabelle can find those files without path reference and we therefore remove all such path references from import statements. With this, `jedit` and `build` should work with and without explicit session context as before. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
99bcebda |
|
07-Jul-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
ASpec: arch-specific faults + VMFault -> ArchFault + ReservedIRQ * fixing name space for arch_tcb and tcb_context * arch_fault added * changing name space for arch_tcb - as_user, set_mrs, get_mrs, copyRegsToArea, and copyRegsToArea are moved to the ARM_HYP directory. This breaks the proofs in refinement, etc., mostly in tcb related files. * removed a duplicate range check definition * fixes ARM for arch_tcb * adding arch_thread_get/set * add ReserveIRQ - initInterruptController is not added yet. * add arch_fault - arch_fault and related functions are added. * arch-parametrising arch-specific extra registers - ArchDefaultExtraRegisters is the common interface that refers to the arch-specific data (ARMNoExtraRegisters for ARM/ARM_HYP) * Adding accesors for tcb_context - Despite the fact that tcb_context has an arch-specific definition, it is reasonable to assume that some form of tcb_context will be available in any architecture, thus the need for accesors to handle updates. * as_user updated to use tcb_context accesors * set_mrs and get_mrs updated to use tcb_context accesors - Several function on ArchTcb_A and ArchTcbAcc_A (both theories where removed) can be defined in a general context by using the tcb_context accesors tags: [VER-623][SELFOUR-413]
|