--- ./bin/pvs-platform.orig 2011-04-15 11:45:09.000000000 -0600 +++ ./bin/pvs-platform 2011-12-06 10:39:21.003660835 -0700 @@ -33,11 +33,8 @@ case `uname -s` in esac os=SunOS os_version=`uname -r | cut -d"." -f1`;; - Linux|FreeBSD) case `uname -m` in - x86_64) arch=ix86_64;; - *86*) arch=ix86;; - esac - os=Linux;; + Linux|FreeBSD) arch=linux + os=Linux;; AIX) arch=powerpc-ibm os=AIX os_version=`uname -r`;; --- ./src/utils/linux/Makefile.orig 2011-12-06 10:39:20.993660845 -0700 +++ ./src/utils/linux/Makefile 2011-12-06 10:39:20.993660845 -0700 @@ -0,0 +1,22 @@ +LDFLAGS = -shared -L./ +CC=gcc +CFLAGS= +SFLAGS=-fPIC -fno-strict-aliasing +VPATH=.. + +obj=file_utils.o + +.SUFFIXES: +.SUFFIXES: .c .o +.c.o : ; $(CC) $(XCFLAGS) $(SFLAGS) $(CFLAGS) -c $< -o $@ + +all : file_utils.so b64 + +file_utils.so: ${obj} + $(CC) $(CFLAGS) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj} + +b64: ../b64.c + $(CC) $(XCFLAGS) $(CFLAGS) -o ./b64 ../b64.c + +clean : + rm -f *.o *.a *.so b64 --- ./src/classes-expr.lisp.orig 2011-04-15 11:45:05.000000000 -0600 +++ ./src/classes-expr.lisp 2011-12-06 10:39:20.992660846 -0700 @@ -36,6 +36,10 @@ ;; SBCL changed things so this no longer works - pvs.system ;; simply unlocks the :common-lisp package +#+sbcl +(eval-when (:execute :compile-toplevel :load-toplevel) + (sb-ext:unlock-package :common-lisp)) + #+cmu (ext:without-package-locks (defgeneric type (x)) --- ./src/WS1S/ws1s-ld-table.orig 2011-04-15 11:45:04.000000000 -0600 +++ ./src/WS1S/ws1s-ld-table 2011-12-06 10:39:20.992660846 -0700 @@ -46,7 +46,7 @@ ws1s___dfaPrintVitals = dfaPrintVitals ; ws1s___dfaPrint = dfaPrint ; ws1s___dfaPrintGraphviz = dfaPrintGraphviz ; ws1s___dfaPrintVerbose = dfaPrintVerbose ; -ws1s___bdd_size = mona_bdd_size ; +ws1s___bdd_size = bdd_size ; ws1s___dfaSetup = dfaSetup ; ws1s___dfaAllocExceptions = dfaAllocExceptions ; ws1s___dfaStoreException = dfaStoreException ; --- ./src/WS1S/linux/Makefile.orig 2011-12-06 10:39:20.991660847 -0700 +++ ./src/WS1S/linux/Makefile 2011-12-06 10:39:20.991660847 -0700 @@ -0,0 +1,55 @@ +ifneq (,) +This makefile requires GNU Make. +endif + +BDD = ../mona/BDD +DFA = ../mona/DFA +UTILS = ../mona/Mem +INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS) +LDFLAGS = -shared -L./ +CC = gcc +CFLAGS += -fPIC -fno-strict-aliasing -D_POSIX_SOURCE -DSYSV $(INCLUDES) +XCFLAGS = -O +SHELL = /bin/sh +VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem + +obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa + +.SUFFIXES: +.SUFFIXES: .c .o +.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ + +all : ws1s.so + +ws1s_extended_interface.o : ../ws1s_extended_interface.c + $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ + +ws1s.so : ${obj} + $(CC) -shared $(XCFLAGS) $(CFLAGS) $(LDFLAGS) -o ws1s.so ${obj} + +bdd.o: bdd.c bdd.h bdd_internal.h +bdd_double.o: bdd_double.c bdd.h bdd_internal.h +bdd_external.o: bdd_external.c bdd_external.h mem.h +bdd_manager.o: bdd_manager.c bdd.h bdd_internal.h +hash.o: hash.c mem.h hash.h +bdd_dump.o: bdd_dump.c bdd_dump.h +bdd_trace.o: bdd_trace.c bdd.h bdd_internal.h +bdd_cache.o: bdd_cache.c bdd.h bdd_internal.h + +analyze.o: analyze.c dfa.h mem.h +prefix.o: prefix.c dfa.h mem.h +product.o: product.c dfa.h bdd.h hash.h mem.h +quotient.o: quotient.c dfa.h hash.h mem.h +basic.o: basic.c dfa.h mem.h +external.o: external.c dfa.h bdd_external.h mem.h +makebasic.o: makebasic.c dfa.h bdd_internal.h +minimize.o: minimize.c dfa.h hash.h mem.h +printdfa.o: printdfa.c dfa.h mem.h +project.o: project.c dfa.h hash.h mem.h +dfa.o: dfa.c dfa.h bdd.h hash.h mem.h + +dlmalloc.o: dlmalloc.c dlmalloc.h +mem.o: mem.c dlmalloc.h + +clean : + rm -f *.o *.a *.so --- ./src/WS1S/ws1s_table.c.orig 2011-04-15 11:45:04.000000000 -0600 +++ ./src/WS1S/ws1s_table.c 2011-12-06 10:39:20.991660847 -0700 @@ -182,8 +182,8 @@ extern int dfaPrintVerbose (int); int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose; -extern int mona_bdd_size (int); -int (*ws1s___bdd_size)(int) = mona_bdd_size; +extern int bdd_size (int); +int (*ws1s___bdd_size)(int) = bdd_size; extern int dfaSetup (int); --- ./Makefile.in.orig 2011-04-15 11:45:09.000000000 -0600 +++ ./Makefile.in 2011-12-06 10:39:21.003660835 -0700 @@ -66,7 +66,7 @@ endif PLATFORM := $(shell $(PVSPATH)bin/pvs-platform) export PLATFORM -bindir = $(TARGETPATH)bin/$(PLATFORM) +bindir = $(TARGETPATH)bin/linux SYSTEM ?= pvs @@ -94,7 +94,7 @@ endif ifneq ($(SBCLISP_HOME),) # Check that the given SBCLISP_HOME works -SBCLISPEXE = $(SBCLISP_HOME)/run-sbcl.sh +SBCLISPEXE = $(SBCLISP_HOME)/sbcl ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK) SBCLVERSION = $(shell $(SBCLISPEXE) --version) # $(warning "$(SBCLVERSION)") @@ -190,10 +190,10 @@ emacs-elc = $(filter-out %ilfsf18.elc %i %illuc19.elc %ilxemacs.elc %ilisp-menu.elc,\ $(emacs-sub-src:.el=.elc)) -ff-files = src/utils/$(PLATFORM)/file_utils.$(LOAD-FOREIGN-EXTENSION) \ - src/utils/$(PLATFORM)/b64 \ - BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) \ - src/WS1S/$(PLATFORM)/ws1s.$(LOAD-FOREIGN-EXTENSION) +ff-files = src/utils/linux/file_utils.$(LOAD-FOREIGN-EXTENSION) \ + src/utils/linux/b64 \ + BDD/linux/mu.$(LOAD-FOREIGN-EXTENSION) \ + src/WS1S/linux/ws1s.$(LOAD-FOREIGN-EXTENSION) ess = ess/dist-ess.lisp \ ess/init-load.lisp \ @@ -502,12 +502,12 @@ $(PVSPATH)TAGS : $(lisp-files) $(allegro $(ETAGS) $(lisp-files) $(allegrolisp) $(sbcllisp) $(cmulisp) $(pvs-emacs-src) fileutils = \ - $(PVSPATH)src/utils/$(PLATFORM)/file_utils.$(LOAD-FOREIGN-EXTENSION) \ - $(PVSPATH)src/utils/$(PLATFORM)/b64 + $(PVSPATH)src/utils/linux/file_utils.$(LOAD-FOREIGN-EXTENSION) \ + $(PVSPATH)src/utils/linux/b64 -bddlib = $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) +bddlib = $(PVSPATH)BDD/linux/mu.$(LOAD-FOREIGN-EXTENSION) -ws1slib = $(PVSPATH)src/WS1S/$(PLATFORM)/ws1s.$(LOAD-FOREIGN-EXTENSION) +ws1slib = $(PVSPATH)src/WS1S/linux/ws1s.$(LOAD-FOREIGN-EXTENSION) image-deps = $(fileutils) $(bddlib) $(ws1slib) $(pvs-make-files) \ $(ess) $(ff-files) $(lisp-files) \ @@ -544,7 +544,7 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp) --eval "(let ((*load-pvs-prelude* nil)) \ (mk:operate-on-system :pvs :compile))" \ --eval '(quit)' - cp $(PVSPATH)src/utils/$(PLATFORM)/b64 $(bindir) + cp $(PVSPATH)src/utils/linux/b64 $(bindir) @echo "******* Building PVS image $@" $(SBCLISPEXE) --eval '(require :sb-posix)' \ --eval '(require :sb-md5)' \ @@ -552,15 +552,14 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp) --eval "(unwind-protect \ (mk:operate-on-system :pvs :compile) \ (save-lisp-and-die \"$@\" \ - :toplevel (function startup-pvs) \ - :executable t))" - -rm $(PVSPATH)BDD/$(PLATFORM)/bdd-sbcl.* + :toplevel (function startup-pvs)))" + -rm $(PVSPATH)BDD/linux/bdd-sbcl.* cp $(SBCLISPEXE) $(subst $(SYSTEM)-sbclisp,,$@) - cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@) + cp $(PVSPATH)BDD/linux/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@) cp $(PVSPATH)BDD/bdd-sbcl.lisp $(PVSPATH)BDD/mu-sbcl.lisp $(subst $(SYSTEM)-sbclisp,,$@) - cp $(PVSPATH)src/WS1S/$(PLATFORM)/ws1s.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@) + cp $(PVSPATH)src/WS1S/linux/ws1s.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@) cp $(PVSPATH)src/WS1S/lisp/dfa-foreign-sbcl.lisp $(subst $(SYSTEM)-sbclisp,,$@) - cp $(PVSPATH)src/utils/$(PLATFORM)/b64 $(bindir) + cp $(PVSPATH)src/utils/linux/b64 $(bindir) endif ifneq ($(CMULISP_HOME),) @@ -635,12 +634,12 @@ endif clean distclean tar $(fileutils) makefileutils : - $(MAKE) -C $(PVSPATH)src/utils/$(PLATFORM) XCFLAGS="$(CFLAGS)" + $(MAKE) -C $(PVSPATH)src/utils/linux XCFLAGS="$(CFLAGS)" $(bddlib) makebdd : - $(MAKE) -C $(PVSPATH)BDD/$(PLATFORM) XCFLAGS="$(CFLAGS)" + $(MAKE) -C $(PVSPATH)BDD/linux XCFLAGS="$(CFLAGS)" $(ws1slib) makews1s : (cd $(PVSPATH)src/WS1S ; rm -rf mona ; ln -s mona-1.4 mona);\ - $(MAKE) -C $(PVSPATH)src/WS1S/$(PLATFORM) XCFLAGS="$(CFLAGS)" + $(MAKE) -C $(PVSPATH)src/WS1S/linux XCFLAGS="$(CFLAGS)" make-release-notes : $(MAKE) -C $(PVSPATH)doc/release-notes --- ./BDD/linux/Makefile.orig 2011-12-06 10:39:20.993660845 -0700 +++ ./BDD/linux/Makefile 2011-12-06 10:39:20.993660845 -0700 @@ -0,0 +1,47 @@ +BDD = ../bdd/src +MU = ../mu/src +UTILS = ../bdd/utils +INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU) +LDFLAGS = -shared -L./ +CC = gcc +CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -fno-strict-aliasing +XCFLAGS = -O +SHELL = /bin/sh +VPATH = ..:../bdd/utils:../bdd/src:../mu/src + +muobj = bdd_interface.o bdd.o bdd_factor.o bdd_quant.o bdd_fns.o bdd_vfns.o \ + appl.o mu_interface.o mu.o + +utilobj = double.o list.o hash.o alloc.o + +.SUFFIXES: +.SUFFIXES: .c .o +.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@ + +all : mu.so + +mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table + $(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm + +libutils.a : ${utilobj} + ar r libutils.a ${utilobj} + ranlib libutils.a + +bdd_interface.o : bdd_interface.c bdd_fns.h +bdd_factor.o : bdd_factor.c bdd_factor.h +bdd.o : bdd.c bdd.h bdd_extern.h +bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h +bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h +bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h + +mu_interface.o : mu_interface.c mu.h +mu.o : mu.c mu.h + +double.o : double.c double.h +list.o : list.c list.h alloc.h +hash.o : hash.c hash.h alloc.h +alloc.o : alloc.c + +clean : + rm -f *.o *.a *.so + --- ./pvs.in.orig 2011-04-15 11:45:09.000000000 -0600 +++ ./pvs.in 2011-12-06 10:42:04.652502258 -0700 @@ -229,15 +229,8 @@ case $opsys in case `uname -m` in x86_64) PVSARCH=ix86_64 ;; *86*) PVSARCH=ix86 ;; - *) echo "PVS only runs on Intel under Linux"; exit 1 + *) PVSARCH=`uname -m` ;; esac - # Allegro does not work with Linux's New Posix Thread Library (NPTL) - # used in newer Red Hat kernels and 2.6 kernels. This will force - # the old thread-implementation. - export LD_ASSUME_KERNEL=2.4.19; - # See if setting this leads to problems - if it does, then - # uname exits with an error and we unset it. - uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL ;; FreeBSD) opsys=Linux majvers= @@ -266,7 +259,7 @@ case $opsys in *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1 esac -binpath=$PVSPATH/bin/$PVSARCH-$opsys${majvers} +binpath=$PVSPATH/bin/linux # Check if this is a 64-bit platform, but only 32-bit available if [ "$PVSARCH" = "ix86_64" -a ! -x "$binpath" ] then binpath=$PVSPATH/bin/ix86-$opsys${majvers} @@ -349,6 +342,7 @@ if [ "$PVSTIMEOUT" -a ! "$batch" ] fi PVSVERBOSE=${PVSVERBOSE:-0} +PVSIMAGE="/usr/bin/sbcl --core $pvsimagepath" export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH export PVSARCH PVSIMAGE PVSPATH PATH PVSLISP PVSVERBOSE PVSTIMEOUT @@ -414,13 +408,13 @@ elif [ $getversion ] then # Make sure there are no spaces in the eval form - otherwise it goes # through the pvs-cmulisp script and gets mangled. - echo `$pvsimagepath $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"` + echo `$PVSIMAGE $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"` elif [ $rawmode ] then if [ -n "$emacsargs" ] then echo "Emacs flags '$emacsargs' will be ignored in raw mode" fi - $pvsimagepath $noinit $flags + $PVSIMAGE $noinit $flags elif [ $batch ] then "$PVSEMACS" $batch $dotemacs $pvsemacsinit $flags 2>&1 --- ./doc/user-guide/user-guide.tex.orig 2011-04-15 11:45:08.000000000 -0600 +++ ./doc/user-guide/user-guide.tex 2011-12-06 10:39:20.994660844 -0700 @@ -20,6 +20,7 @@ \else \usepackage[bookmarks=true,hyperindex=true]{hyperref} \fi +\usepackage{amssymb} \topmargin -10pt \textheight 8.5in