This file is indexed.

/usr/share/acl2-4.3/books/make-event/assert.lisp is in acl2-books-source 4.3-3.

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
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
; The macro assert!, defined and illustrated below, allows for assertions
; within an ACL2 book, as requested by David Rager.

(in-package "ACL2")

(defun assert!-body (assertion form)

; Note that assertion should evaluate to a single non-stobj value.  See also
; assert!-stobj-body.

  `(let ((assertion ,assertion))
     (er-progn
      (if assertion
          (value nil)
        (er soft 'assert!
            "Assertion failed:~%~x0"
            ',assertion))
      (value ',(or form '(value-triple :success))))))

(defmacro assert! (&whole whole-form
                          assertion &optional form)

; Note that assertion should evaluate to a single non-stobj value.  See also
; assert!-stobj.

  (list 'make-event (assert!-body assertion form)
        :on-behalf-of whole-form))

(assert! (equal 3 3)
         (defun assert-test1 (x) x))

; Check that above defun was evaluated.
(value-triple (or (equal (assert-test1 3) 3)
                  (er hard 'top-level
                      "Failed to evaluate (assert-test1 3) to 3.")))

(include-book "eval")

(must-fail
 (assert! (equal 3 4)
          (defun assert-test2 (x) x)))

; Check that above defun was not evaluated.
(defun assert-test2 (x)
  (cons x x))

; Simple test with no second argument:
(assert! (equal (append '(a b c) '(d e f))
                '(a b c d e f)))

; Check failure of assertion when condition is false:
(must-fail
 (assert! (equal (append '(a b c) '(d e f))
                 '(a b))))

; The following requires that this book be certified in the initial
; certification world.  It also succeeds at include-book time even if we
; include the book after executing another command, because assert! uses
; make-event with :check-expansion nil.  See assert-include.lisp.
(local (assert! (equal (access-command-tuple-form
                        (cddr (car (scan-to-command (w state)))))
                       '(exit-boot-strap-mode))))

; We turn now to developing an extension of assert! that works with stobjs, in
; this case for assertions that return (mv val st) where val is an ordinary
; value and st is a stobj.  Our intention is to illustrate how to write other
; versions of assert!.  If you understand this extension, you can then write
; your own extensions that can similarly handle other signatures for the
; assertion.

(defun assert!-stobj-body (assertion st form)

; Assertion should evaluate to (mv val st), where val is an ordinary value and
; st is a stobj.  See also assert!-body.

  `(mv-let (result ,st)
           ,assertion
           (if result
               (mv nil ',(or form '(value-triple :success)) state ,st)
             (mv-let (erp val state)
                     (er soft 'assert!
                         "Assertion failed:~%~x0"
                         ',assertion)
                     (declare (ignore erp val))
                     (mv t nil state ,st)))))

(defmacro assert!-stobj (&whole whole-form
                                assertion st &optional form)

; Assertion should evaluate to (mv val st), where val is an ordinary value and
; st is a stobj.  See also assert!.

  (list 'make-event (assert!-stobj-body assertion st form)
        :on-behalf-of whole-form))

; Test-stobj example from David Rager.
(local
 (encapsulate
  ()

  (defstobj foo field1 field2)

  (defun test-stobj (x foo)
    (declare (xargs :stobjs foo))
    (let ((foo (update-field1 17 foo)))
      (update-field2 x foo)))

; Passes.
  (assert!-stobj (let* ((foo (test-stobj 14 foo)))
                   (mv (equal (field1 foo)
                              17)
                       foo))
                 foo)

  (must-fail
   (assert!-stobj (let* ((foo (test-stobj 14 foo)))
                    (mv (equal (field1 foo)
                               14)
                        foo))
                  foo))
  ))