From 8388ac10289d5cab791953238057294604af6d60 Mon Sep 17 00:00:00 2001
From: Matt Kaufmann <kaufmann@cs.utexas.edu>
Date: Sat, 14 Jul 2018 10:07:13 -0500
Subject: [PATCH] Fixed read-file-into-string bug.

Quoting :doc note-8-1:

  A bug has been fixed in the logical definition of the function,
  read-file-into-string2, which supports the macro,
  [read-file-into-string].  Thanks to Keshav Kini for finding this
  bug and to Mihir Mehta for a query leading to Keshav's
  investigation.
---
 books/system/doc/acl2-doc.lisp |  5 +++++
 doc.lisp                       | 12 +++++++++---
 other-events.lisp              |  6 +++---
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp
index dfb07365920..1887f89ee78 100644
--- a/books/system/doc/acl2-doc.lisp
+++ b/books/system/doc/acl2-doc.lisp
@@ -80621,6 +80621,11 @@ it."
  (MV X X) is 1 but the actual number of return values is 2.''  This has been
  fixed.  Thanks to Eric Smith for bringing this problem to our attention.</p>
 
+ <p>A bug has been fixed in the logical definition of the function,
+ @('read-file-into-string2'), which supports the macro, @(tsee
+ read-file-into-string).  Thanks to Keshav Kini for finding this bug and to
+ Mihir Mehta for a query leading to Keshav's investigation.</p>
+
  <h3>Changes at the System Level</h3>
 
  <p>Fixed the use of `@('<a href='URL'>...</a>')' so that if @('URL') has the
diff --git a/doc.lisp b/doc.lisp
index 810fff3915e..6b6aec12053 100644
--- a/doc.lisp
+++ b/doc.lisp
@@ -79104,6 +79104,12 @@ Bug Fixes
   2.'' This has been fixed.  Thanks to Eric Smith for bringing this
   problem to our attention.
 
+  A bug has been fixed in the logical definition of the function,
+  read-file-into-string2, which supports the macro,
+  [read-file-into-string].  Thanks to Keshav Kini for finding this
+  bug and to Mihir Mehta for a query leading to Keshav's
+  investigation.
+
 
 Changes at the System Level
 
@@ -90610,10 +90616,10 @@ Subtopics
                               (mv nil val state)))))))
          (mv erp
              (and (stringp val)
-                  (<= start (len val))
+                  (<= start (length val))
                   (subseq val start
-                          (if bytes (min (+ start bytes) (len val))
-                              (len val)))))))
+                          (if bytes (min (+ start bytes) (length val))
+                              (length val)))))))
        (declare (ignore erp))
        val)))
 
diff --git a/other-events.lisp b/other-events.lisp
index 9cdb9b11111..cb65515c9b1 100644
--- a/other-events.lisp
+++ b/other-events.lisp
@@ -30167,13 +30167,13 @@
 ; If the following conjunct is false, then raw Lisp would cause an error; so
 ; there is no harm in adding it (and, it helps with guard verification).
 
-                  (<= start (len val))
+                  (<= start (length val))
                   (subseq val
                           start
                           (if bytes
                               (min (+ start bytes)
-                                   (len val))
-                            (len val)))))))
+                                   (length val))
+                            (length val)))))))
       (declare (ignore erp))
       val)))
 )