1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7chapter "Tools"
8
9session AsmRefine = CParser +
10  sessions
11    Word_Lib
12    Lib
13    CLib
14  directories
15    "$L4V_ARCH"
16  theories
17    GraphProof
18    ProveGraphRefine
19    GhostAssertions
20    SimplExport
21
22session AsmRefineTest in "testfiles" = AsmRefine +
23  options [threads = 1] (* use of unsync references in test files *)
24  sessions
25    CParser
26  theories
27    "global_asm_stmt_gref"
28    "inf_loop_gref"
29    "global_array_swap_gref"
30