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

@@ -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

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)))
 

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)))
 )