l4v
l4v copied to clipboard
seL4
seL4 specification and proofs
I cloned this repo and executed this command "./build.sh -b l4v", then got message : ``` ..... cabal-install > Linking .stack-work/dist/x86_64-linux-tinfo6/Cabal-3.4.1.0/build/cabal/cabal ... cabal-install > copy/register cabal-install > Installing executable cabal...
This tactic deals with heap updates in the context of lift_t, turning UMM heap_updates into function updates to the lift_t, or removing them completely if the update doens't interact with...
This modifies the tcb_decode functions so that it is possible to set the badge and rights of fault and timeout handler caps, and updates ainvs for riscv. See https://sel4.atlassian.net/browse/RFC-11 for...
Raf's idea: one thing that is annoying to type in `crunches` is longer lambda expressions in `crunches`, e.g. the common pattern "%s. P (machine_state s)" We could add syntax for...
In the abstract specification we had put a lot of VCPU content into ArchVSpace and ArchVSpaceAcc, even though VCPUs aren't really very related to VSpace. This content has now been...
We currently have multiple word types in the abstract spec (and others) that are type synonyms with `machine_word` (`obj_ref`, `paddr`, `vspace_ref` etc). This means we get different names in input,...
It would be convenient to have direct and automatic access to the sizes of C structs in the higher level specs, namely the abstract spec and the design spec, and...