/usr/share/acl2-8.0dfsg/books/system/check-system-guards.lisp is in acl2-books-source 8.0dfsg-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 | ; Copyright (C) 2017, Regents of the University of Texas
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This books runs (add-guards-as-assertions-all), which checks top-level calls
; of built-in functions that are in :logic mode, guard-verified. That check is
; done on (mini-proveall) after a more limiated check,
; (add-guards-as-assertions-svga), check just those functions that are
; guard-verified outside the system, i.e., are in *system-verify-guards-alist*.
; Those checks can be done without this book, by just loading its workhorse,
; check-system-guards-raw.lsp, as follows. First do the set-up:
; :q
; (load "check-system-guards-raw.lsp")
; (add-guards-as-assertions-all)
; (lp)
; Now execute some forms, e.g.:
; (mini-proveall)
; :ubt 1
; (time$ (include-book "arithmetic/top" :dir :system))
; Finally, to see that guards were indeed being checked:
; (report-guard-checks)
; This book does some of that automatically, as a bit of a check during
; regression on guards of guard-verified system functions.
(in-package "ACL2")
(local (include-book "tools/include-raw" :dir :system))
(defttag :check-system-guards)
(local (include-raw "check-system-guards-raw.lsp"))
(local (progn!
(set-raw-mode t)
(add-guards-as-assertions-svga)))
; The following may take a couple of minutes.
(local (include-book "arithmetic-5/top" :dir :system))
(local (progn!
(set-raw-mode t)
(add-guards-as-assertions-all)))
; This should go quickly.
(local (progn! (assign ld-okp t)
(mini-proveall)))
; We can report results during both passes of certification.
(progn! (set-raw-mode t)
(report-guard-checks))
|