adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec
History
Gerwin Klein 83ddb4def9
aarch64 ainvs: remove unused physBase lemmas (#625) 
The condition `pptrBase < kernelELFBase` is not required on AArch64 in
hyp mode and was left over from the initial RISC-V setup.

Since this check does fail for some platforms (where physBase = 0 and
consequently pptrBase = kernelELFBase) we remove it here.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2023-04-05 13:50:33 +10:00
..
abstract READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
capDL READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
cspec READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
design READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
haskell aarch64 haskell: eliminate isValidNativeRoot 2023-03-09 10:15:19 +11:00
machine aarch64 ainvs: remove unused physBase lemmas (#625) 2023-04-05 13:50:33 +10:00
sep-abstract READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
take-grant READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
Makefile Makefiles: remove unused report-regression target 2022-06-03 09:36:43 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT isabelle2021-1: DSpec 2022-03-29 08:38:25 +11:00
tests.xml tests: add kernel-config session (#614) 2023-03-21 13:50:37 +11:00

README.md

Formal Specifications of seL4

See the sub directories for more details.

The Makefile and ROOT file define runnable Isabelle sessions for these specifications.