1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11chapter "Specifications" 12 13(* 14 * List of rules to make various images. 15 * 16 * Some rules have duplicate targets of the form: 17 * 18 * theories [condition = "MOO", quick_and_dirty] 19 * "foo" 20 * theories 21 * "foo" 22 * 23 * The idea is that if the environment variable "MOO" is defined we 24 * execute the first rule (doing the proof in quick-and-dirty mode), and 25 * then find we need not take any action for the second. Otherwise, we 26 * skip the first rule and only perform the second. 27 *) 28 29(* 30 * Abstract Specification 31 *) 32 33(* Session on which most other sessions build. *) 34session ASpec in "abstract" = Word_Lib + 35 options [document=false] 36 sessions 37 "HOL-Library" 38 Lib 39 ExecSpec 40 theories 41 "Syscall_A" 42 43(* We build the abstract specification document in a separate session, 44 to avoid rebuilding ASpec (and every session that depends on it) 45 whenever the git commit ID changes. *) 46session ASpecDoc in "abstract" = Word_Lib + 47 options [document=pdf] 48 sessions 49 "HOL-Library" 50 Lib 51 ExecSpec 52 theories 53 "Intro_Doc" 54 theories 55 "Syscall_A" 56 "Glossary_Doc" 57 (* "KernelInit_A" *) 58 document_files 59 "VERSION" (* generated by `make ASpec` *) 60 "gitrev.tex" (* generated by `make ASpec` *) 61 "root.tex" 62 "root.bib" 63 "defs.bib" 64 "ulem.sty" 65 "imgs/CDT.pdf" 66 "imgs/seL4-background_01.pdf" 67 "imgs/seL4-background_03.pdf" 68 "imgs/seL4-background_04.pdf" 69 "imgs/sel4objects_01.pdf" 70 "imgs/sel4objects_05.pdf" 71 "imgs/sel4_internals_01.pdf" 72 document_files (in "document/$L4V_ARCH") 73 "ARCH.tex" 74 75(* 76 * Executable/Design Specification 77 *) 78 79session ExecSpec = Word_Lib + 80 options [document = false] 81 sessions 82 Lib 83 "HOL-Eisbach" 84 theories 85 "design/API_H" 86 "design/$L4V_ARCH/ArchIntermediate_H" 87 88 89(* 90 * C Kernel 91 *) 92 93session CSpec = CKernel + 94 theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty] 95 "cspec/Substitute" 96 theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty] 97 "cspec/KernelInc_C" 98 theories 99 "cspec/KernelInc_C" 100 "cspec/KernelState_C" 101 102session CKernel = CParser + 103 sessions 104 "ExecSpec" 105 "CLib" 106 "AsmRefine" 107 theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty] 108 "cspec/$L4V_ARCH/Kernel_C" 109 theories 110 "cspec/$L4V_ARCH/Kernel_C" 111 112 113(* 114 * CapDL 115 *) 116 117session DSpec in capDL = Word_Lib + 118 sessions 119 ExecSpec 120 ASpec 121 theories 122 Syscall_D 123 124 125(* 126 * Take-Grant. 127 *) 128 129session TakeGrant in "take-grant" = Word_Lib + 130 theories 131 "System_S" 132 "Isolation_S" 133 "Example" 134 "Example2" 135 136 137(* 138 * Separation Kernel Setup Specification 139 *) 140 141session ASepSpec = ASpec + 142 options [document = false] 143 theories 144 "sep-abstract/Syscall_SA" 145 146