[Gcl-devel] Re: minor gcl bug?

[Camm Maguire]

Greetings, and thanks for your report!

I believe this has been fixed in recent CVS (at least with Debian
package version -70, and probably quite a bit earlier)

Here is what I get -- please let me know if it still does not work for you:

=============================================================================
intech19:/fix/t1/camm/tmp/acl2-2.7/tmp$ ls
foo.cert  foo.lisp  foo.o  regexp.h
intech19:/fix/t1/camm/tmp/acl2-2.7/tmp$ ../saved_acl2
GCL (GNU Common Lisp)  Version(2.5.0) Fri Jan  3 15:23:43 EST 2003
Licensed under GNU Library General Public License
Contains Enhancements by W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.7 built January 3, 2003  15:44:57.
 Copyright (C) 2002  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T).
 See the documentation topic note-2-7 for recent changes.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc; 
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 2.7.  Level 1.  Cbd "/fix/t1/camm/tmp/acl2-2.7/tmp/".
Type :help for help.

ACL2 !>(certify-book "foo")

CERTIFICATION ATTEMPT FOR "/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp"
ACL2 Version 2.7


* Step 1:  Read "/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp" and compute
its check sum.

* Step 2:  There were two forms in the file. The check sum is 43986201.
We now attempt to establish that each form, whether local or non-local,
is indeed an admissible embedded event form in the context of the previously
admitted ones.  Note that proof-tree output is inhibited during this
check; see :DOC proof-tree.


ACL2 !>>(DEFUN FOO (X) X)

Since FOO is non-recursive, its admission is trivial.  We observe that
the type of FOO is described by the theorem (EQUAL (FOO X) X).  

Summary
Form:  ( DEFUN FOO ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOO

* Step 3:  That completes the admissibility check.  Each form read
was an embedded event form and was admissible. We now retract back
to the initial world and try to include the book.  This may expose
local incompatibilities.

Summary
Form:  ( INCLUDE-BOOK "foo" ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Warning [Guards] in (CERTIFY-BOOK "foo" ...):  You have told certify-
book to produce a compiled file for "/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp".
However, the function FOO has not had its guards verified.  A compiled
file will be produced anyway, but all bets are off if you load it into
raw Common Lisp and try to run the functions in it.  See :DOC verify-
guards.


* Step 4:  Write the certificate for 
"/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp" in 
"/fix/t1/camm/tmp/acl2-2.7/tmp/foo.cert".  The final check sum alist
is 
(("/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp"
      "foo"
      "foo" ((:SKIPPED-PROOFSP) (:AXIOMSP))
      . 43986201)).


* Step 5:  Compile the functions defined in 
"/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp".  As noted above, one function
has not had its guard verified.  A compiled file will be produced but
you are advised not to use it in raw Common Lisp.  See :DOC guard for
a general discussion of the issues.
Compiling /fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp.
End of Pass 1.  
End of Pass 2.  
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /fix/t1/camm/tmp/acl2-2.7/tmp/foo.o.

"/fix/t1/camm/tmp/acl2-2.7/tmp/foo.o" 

Loading /fix/t1/camm/tmp/acl2-2.7/tmp/foo.o
start address -T 0x9810f54 Finished loading /fix/t1/camm/tmp/acl2-2.7/tmp/foo.o

Summary
Form:  (CERTIFY-BOOK "foo" ...)
Rules: NIL
Warnings:  Guards
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 "/fix/t1/camm/tmp/acl2-2.7/tmp/foo.lisp"
=============================================================================

Take care,


Matt Kaufmann <address@hidden> writes:

> I've discovered a minor problem with GCL 2.5.0 while using ACL2 Version 2.7 on
> a Debian Gnu Linux machine at UT (craigievar) -- unfortunately I don't know
> which 2.5.0 was installed (maybe such sub-version info is stored in a global
> variable?).  There just happened to be a file regexp.h in the current 
> directory
> where I attempted to certify a book.  Compilation broke unless I moved or
> deleted that regexp.h.  I don't know why regexp.h was there, but I'm surprised
> that it matters whether such a file is in the local directory.
> 
> Below are the book foo.lisp to be certified (I think most any book will do) 
> and
> the regexp.h.
> 
> ============================== foo.lisp ==============================
> 
> (in-package "ACL2")
> 
> (defun foo (x)
>   x)
> 
> ============================== regexp.h ==============================
> 
> /* Copyright (C) 1996, 1997, 1998, 1999 Free Software Foundation, Inc.
>    This file is part of the GNU C Library.
>    Contributed by Ulrich Drepper <address@hidden>, 1996.
> 
>    The GNU C Library is free software; you can redistribute it and/or
>    modify it under the terms of the GNU Lesser General Public
>    License as published by the Free Software Foundation; either
>    version 2.1 of the License, or (at your option) any later version.
> 
>    The GNU C Library 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 GNU
>    Lesser General Public License for more details.
> 
>    You should have received a copy of the GNU Lesser General Public
>    License along with the GNU C Library; if not, write to the Free
>    Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
>    02111-1307 USA.  */
> 
> #ifndef _REGEXP_H
> #define _REGEXP_H     1
> 
> /* The contents of this header file was first standardized in X/Open
>    System Interface and Headers Issue 2, originally coming from SysV.
>    In issue 4, version 2, it is marked as TO BE WITDRAWN.
> 
>    This code shouldn't be used in any newly written code.  It is
>    included only for compatibility reasons.  Use the POSIX definition
>    in <regex.h> for portable applications and a reasonable interface.  */
> 
> #include <features.h>
> #include <alloca.h>
> #include <regex.h>
> #include <stdlib.h>
> #include <string.h>
> 
> /* The implementation provided here emulates the needed functionality
>    by mapping to the POSIX regular expression matcher.  The interface
>    for the here included function is weird (this really is a harmless
>    word).
> 
>    The user has to provide six macros before this header file can be
>    included:
> 
>    INIT               Declarations vor variables which can be used by the
>               other macros.
> 
>    GETC()     Return the value of the next character in the regular
>               expression pattern.  Successive calls should return
>               successive characters.
> 
>    PEEKC()    Return the value of the next character in the regular
>               expression pattern.  Immediately successive calls to
>               PEEKC() should return the same character which should
>               also be the next character returned by GETC().
> 
>    UNGETC(c)  Cause `c' to be returned by the next call to GETC() and
>               PEEKC().
> 
>    RETURN(ptr)        Used for normal exit of the `compile' function.  `ptr'
>               is a pointer to the character after the last character of
>               the compiled regular expression.
> 
>    ERROR(val) Used for abnormal return from `compile'.  `val' is the
>               error number.  The error codes are:
>               11      Range endpoint too large.
>               16      Bad number.
>               25      \digit out of range.
>               36      Illegal or missing delimiter.
>               41      No remembered search string.
>               42      \( \) imbalance.
>               43      Too many \(.
>               44      More tan two numbers given in \{ \}.
>               45      } expected after \.
>               46      First number exceeds second in \{ \}.
>               49      [ ] imbalance.
>               50      Regular expression overflow.
> 
>   */
> 
> __BEGIN_DECLS
> 
> /* Interface variables.  They contain the results of the successful
>    calls to `setp' and `advance'.  */
> extern char *loc1;
> extern char *loc2;
> 
> /* The use of this variable in the `advance' function is not
>    supported.  */
> extern char *locs;
> 
> 
> #ifndef __DO_NOT_DEFINE_COMPILE
> /* Get and compile the user supplied pattern up to end of line or
>    string or until EOF is seen, whatever happens first.  The result is
>    placed in the buffer starting at EXPBUF and delimited by ENDBUF.
> 
>    This function cannot be defined in the libc itself since it depends
>    on the macros.  */
> char *
> compile (char *__restrict instring, char *__restrict expbuf,
>        __const char *__restrict endbuf, int eof)
> {
>   char *__input_buffer = NULL;
>   size_t __input_size = 0;
>   size_t __current_size = 0;
>   int __ch;
>   int __error;
>   INIT
> 
>   /* Align the expression buffer according to the needs for an object
>      of type `regex_t'.  Then check for minimum size of the buffer for
>      the compiled regular expression.  */
>   regex_t *__expr_ptr;
> # if defined __GNUC__ && __GNUC__ >= 2
>   const size_t __req = __alignof__ (regex_t *);
> # else
>   /* How shall we find out?  We simply guess it and can change it is
>      this really proofs to be wrong.  */
>   const size_t __req = 8;
> # endif
>   expbuf += __req;
>   expbuf -= (expbuf - ((char *) 0)) % __req;
>   if (endbuf < expbuf + sizeof (regex_t))
>     {
>       ERROR (50);
>     }
>   __expr_ptr = (regex_t *) expbuf;
>   /* The remaining space in the buffer can be used for the compiled
>      pattern.  */
>   __expr_ptr->buffer = expbuf + sizeof (regex_t);
>   __expr_ptr->allocated = endbuf -  (char *) __expr_ptr->buffer;
> 
>   while ((__ch = (GETC ())) != eof)
>     {
>       if (__ch == '\0' || __ch == '\n')
>       {
>         UNGETC (__ch);
>         break;
>       }
> 
>       if (__current_size + 1 >= __input_size)
>       {
>         size_t __new_size = __input_size ? 2 * __input_size : 128;
>         char *__new_room = (char *) alloca (__new_size);
>         /* See whether we can use the old buffer.  */
>         if (__new_room + __new_size == __input_buffer)
>           {
>             __input_size += __new_size;
>             __input_buffer = (char *) memcpy (__new_room, __input_buffer,
>                                              __current_size);
>           }
>         else if (__input_buffer + __input_size == __new_room)
>           __input_size += __new_size;
>         else
>           {
>             __input_size = __new_size;
>             __input_buffer = (char *) memcpy (__new_room, __input_buffer,
>                                               __current_size);
>           }
>       }
>       __input_buffer[__current_size++] = __ch;
>     }
>   __input_buffer[__current_size++] = '\0';
> 
>   /* Now compile the pattern.  */
>   __error = regcomp (__expr_ptr, __input_buffer, REG_NEWLINE);
>   if (__error != 0)
>     /* Oh well, we have to translate POSIX error codes.  */
>     switch (__error)
>       {
>       case REG_BADPAT:
>       case REG_ECOLLATE:
>       case REG_ECTYPE:
>       case REG_EESCAPE:
>       case REG_BADRPT:
>       case REG_EEND:
>       case REG_ERPAREN:
>       default:
>       /* There is no matching error code.  */
>       RETURN (36);
>       case REG_ESUBREG:
>       RETURN (25);
>       case REG_EBRACK:
>       RETURN (49);
>       case REG_EPAREN:
>       RETURN (42);
>       case REG_EBRACE:
>       RETURN (44);
>       case REG_BADBR:
>       RETURN (46);
>       case REG_ERANGE:
>       RETURN (11);
>       case REG_ESPACE:
>       case REG_ESIZE:
>       ERROR (50);
>       }
> 
>   /* Everything is ok.  */
>   RETURN ((char *) (__expr_ptr->buffer + __expr_ptr->used));
> }
> #endif
> 
> 
> /* Find the next match in STRING.  The compiled regular expression is
>    found in the buffer starting at EXPBUF.  `loc1' will return the
>    first character matched and `loc2' points to the next unmatched
>    character.  */
> extern int step (__const char *__restrict __string,
>                __const char *__restrict __expbuf) __THROW;
> 
> /* Match the beginning of STRING with the compiled regular expression
>    in EXPBUF.  If the match is successful `loc2' will contain the
>    position of the first unmatched character.  */
> extern int advance (__const char *__restrict __string,
>                   __const char *__restrict __expbuf) __THROW;
> 
> 
> __END_DECLS
> 
> #endif /* regexp.h */
> 
> ==============================
> 
> Thanks --
> -- Matt
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah