This file is indexed.

/usr/share/acl2-7.2dfsg/serialize.lisp is in acl2-source 7.2dfsg-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
122
; ACL2 Version 7.2 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2016, Regents of the University of Texas

; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; LICENSE for more details.

; Regarding authorship of ACL2 in general:

; Written by:  Matt Kaufmann               and J Strother Moore
; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.

; serialize.lisp -- logical definitions for "serialization" routines,
;                   i.e., saving ACL2 objects in files for later loading

; This file was developed and contributed by Jared Davis on behalf of
; Centaur Technology.

; Note: The serialization routines are restricted to work only in
; ACL2(h).  However, they are independent of the remainder of the HONS
; extension and might some day become part of ordinary ACL2.

; Please direct correspondence about this file to Jared Davis
; <jared@centtech.com>.

(in-package "ACL2")

(defmacro serialize-write (filename obj &key verbosep)
  `(serialize-write-fn ,filename ,obj ,verbosep state))

(defun serialize-write-fn (filename obj verbosep state)
  (declare (xargs :guard (and (stringp filename)
                              (booleanp verbosep)
                              (state-p state))
                  :stobjs state)
           (ignorable filename obj verbosep))
  #-acl2-loop-only
  (cond
   ((live-state-p state)
    #-hons
    (er hard? 'serialize-write-fn
        "Serialization routines are currently only available in the HONS ~
         version of ACL2.")
    #+hons
    (with-open-file
     (stream filename
             :direction :output
             :if-exists :supersede)
     (let* ((*ser-verbose* verbosep))
       (ser-encode-to-stream obj stream)))
    (return-from serialize-write-fn state))
   (t

; We fall through to the logic code if we are doing a proof, where
; *hard-error-returns-nilp* is true.  Otherwise, we throw here with an error
; message.

    (er hard? 'serialize-write-fn "Serialization requires a live state.")))
  (mv-let (erp val state)
          (read-acl2-oracle state)
          (declare (ignore erp val))
          state))

(defmacro serialize-read (filename &key
                                   (hons-mode ':smart)
                                   verbosep)
  `(serialize-read-fn ,filename ,hons-mode ,verbosep state))

(defun serialize-read-fn (filename hons-mode verbosep state)

; This function returns a single object.

  (declare (xargs :guard (and (stringp filename)
                              (member hons-mode '(:never :always :smart))
                              (booleanp verbosep)
                              (state-p state))
                  :stobjs state)
           (ignorable filename hons-mode verbosep))

  #-acl2-loop-only
  (cond
   ((live-state-p state)
    (return-from
     serialize-read-fn
     #-hons
     (progn (er hard? 'serialize-read-fn
                "Serialization routines are currently only available in the ~
                 HONS version of ACL2.")
            (mv nil state))
     #+hons
     (with-open-file
      (stream filename :direction :input)
      (let* ((*ser-verbose* verbosep)
             (val           (ser-decode-from-stream t hons-mode stream)))
        (mv val state)))))
   (t

; We fall through to the logic code if we are doing a proof, where
; *hard-error-returns-nilp* is true.  Otherwise, we throw here with an error
; message.

    (er hard? 'serialize-read-fn "Serialization requires a live state.")))
  (mv-let (erp val state)
          (read-acl2-oracle state)
          (declare (ignore erp))
          (mv val state)))

(defmacro with-serialize-character (val form)
  (declare (xargs :guard (member val '(nil #\Y #\Z))))
  `(state-global-let*
    ((serialize-character ,val set-serialize-character))
    ,form))