139 lines
2.6 KiB
Plaintext
139 lines
2.6 KiB
Plaintext
(*
|
|
* Copyright 2014, General Dynamics C4 Systems
|
|
*
|
|
* SPDX-License-Identifier: GPL-2.0-only
|
|
*)
|
|
|
|
chapter "Specifications"
|
|
|
|
(*
|
|
* List of rules to make various images.
|
|
*
|
|
* Some rules have duplicate targets of the form:
|
|
*
|
|
* theories [condition = "MOO", quick_and_dirty]
|
|
* "foo"
|
|
* theories
|
|
* "foo"
|
|
*
|
|
* The idea is that if the environment variable "MOO" is defined we
|
|
* execute the first rule (doing the proof in quick-and-dirty mode), and
|
|
* then find we need not take any action for the second. Otherwise, we
|
|
* skip the first rule and only perform the second.
|
|
*)
|
|
|
|
(*
|
|
* Abstract Specification
|
|
*)
|
|
|
|
(* Session on which most other sessions build. *)
|
|
session ASpec in "abstract" = Word_Lib_l4v +
|
|
options [document=pdf]
|
|
sessions
|
|
"HOL-Library"
|
|
Lib
|
|
ExecSpec
|
|
directories
|
|
"$L4V_ARCH"
|
|
theories
|
|
"Syscall_A"
|
|
"Intro_Doc"
|
|
"Glossary_Doc"
|
|
(* "KernelInit_A" *)
|
|
document_files
|
|
"VERSION.tex" (* generated by `make ASpec` *)
|
|
"git-root.tex" (* generated by `make ASpec` *)
|
|
"root.tex"
|
|
"root.bib"
|
|
"defs.bib"
|
|
"ulem.sty"
|
|
"imgs/CDT.pdf"
|
|
"imgs/seL4-background_01.pdf"
|
|
"imgs/seL4-background_03.pdf"
|
|
"imgs/seL4-background_04.pdf"
|
|
"imgs/sel4objects_01.pdf"
|
|
"imgs/sel4objects_05.pdf"
|
|
"imgs/sel4_internals_01.pdf"
|
|
document_files (in "document/$L4V_ARCH")
|
|
"ARCH.tex"
|
|
|
|
(*
|
|
* Executable/Design Specification
|
|
*)
|
|
|
|
session ExecSpec in "design" = Word_Lib_l4v +
|
|
options [document = false]
|
|
sessions
|
|
Lib
|
|
"HOL-Eisbach"
|
|
directories
|
|
"$L4V_ARCH"
|
|
"../machine"
|
|
"../machine/$L4V_ARCH"
|
|
theories
|
|
"API_H"
|
|
"$L4V_ARCH/ArchIntermediate_H"
|
|
|
|
|
|
(*
|
|
* C Kernel
|
|
*)
|
|
|
|
session CSpec in "cspec" = CKernel +
|
|
directories
|
|
"c/build/$L4V_ARCH/generated/arch/object"
|
|
"c/build/$L4V_ARCH/generated/sel4"
|
|
theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
|
|
"Substitute"
|
|
theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty]
|
|
"KernelInc_C"
|
|
theories
|
|
"KernelInc_C"
|
|
"KernelState_C"
|
|
|
|
session CKernel in "cspec/$L4V_ARCH" = CParser +
|
|
sessions
|
|
"ExecSpec"
|
|
"CLib"
|
|
"AsmRefine"
|
|
theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
|
|
"Kernel_C"
|
|
theories
|
|
"Kernel_C"
|
|
|
|
|
|
(*
|
|
* CapDL
|
|
*)
|
|
|
|
session DSpec in capDL = Word_Lib_l4v +
|
|
sessions
|
|
ExecSpec
|
|
ASpec
|
|
"HOL-Combinatorics" (* for Fun.swap *)
|
|
theories
|
|
Syscall_D
|
|
|
|
|
|
(*
|
|
* Take-Grant.
|
|
*)
|
|
|
|
session TakeGrant in "take-grant" = Word_Lib_l4v +
|
|
theories
|
|
"System_S"
|
|
"Isolation_S"
|
|
"Example"
|
|
"Example2"
|
|
|
|
|
|
(*
|
|
* Separation Kernel Setup Specification
|
|
*)
|
|
|
|
session ASepSpec in "sep-abstract" = ASpec +
|
|
options [document = false]
|
|
theories
|
|
"Syscall_SA"
|
|
|