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