--- ./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