[Gcl-devel] Re: enable-debug

[Camm Maguire]

Greetings!

OK, the compile problem is now fixed -- still looking at the extranous
values returned by compile-file with C optimization on.

Take care,

Robert Boyer <address@hidden> writes:

> Here's a rather pointless message.
> 
> As you suggested, I rebuilt with enable-debug and ran under gdb and got an
> error at the same place in ACL2 compilation, though this time called
> 'segmentation violation' rather than 'stack overflow'.  Below is a partial
> transcript, and then a couple of comments.
> 
> Bob
> 
> ;; Compiling interface-raw.lisp.
> ; (DEFUN ACL2-GENTEMP ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> (VALUES T
>                                                               T)
> 
> ; (DEFUN CHECK-ACL2-WORLD-INVARIANT ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
> 
> ; (DEFUN CHK-VIRGIN2 ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
> 
> ; (DEFUN CHK-PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS2 ...) is being 
> compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
> 
> ; (DEFUN CHECK-BUILT-IN-CONSTANTS ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
> 
> ; (DEFUN STOBJ-PRINT-SYMBOL ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> (VALUES T
>                                                               T)
> 
> ; (DEFUN SAVED-BUILD-DATE-STRING ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
> 
> ;; End of Pass 1.  
> 
> Program received signal SIGSEGV, Segmentation fault.
> 0x083bed22 in LI157 (V4812=0x349e76b8, V4813=0x24b27b60, V4814=0x9ebe7d8, 
>     V4815=0xb5fa8c8) at gcl_recompile.c:27809
> 27809         V4863= make_cons(CMPcadr(CMPcar((V4862))),Cnil);
> (gdb) (gdb) 
> 
> 
>   -rwxr-xr-x   1 boyer prof   3724 Jul 12 22:04 gcl_profile.lsp
>   -rw-r--r--   1 boyer prof    156 Jul 12 22:04 gcl_recompile.c
>   -rw-r--r--   1 boyer prof    112 Jul 12 22:04 gcl_recompile.data
>   -rw-r--r--   1 boyer prof     66 Jul 12 22:04 gcl_recompile.h
>   -rw-r--r--   1 boyer prof      0 Jul 12 22:04 gcl_recompile.lsp
>   -rw-r--r--   1 boyer prof  29148 Jul 12 22:04 gcl_recompile.o
> 
> which is strange to me because gcl_recompile.lsp is an empty file and
> gcl_recompile.c does not have very many lines, certainly not 27809.
> 
> #include "cmpinclude.h"
> #include "gcl_recompile.h"
> void init_gcl_recompile(){do_init((void *)VV);}
> 
> #ifdef SYSTEM_SPECIAL_INIT
> SYSTEM_SPECIAL_INIT
> #endif
> 
> 
> 
> 

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