Sophie

Sophie

distrib > Fedora > 18 > x86_64 > by-pkgid > a16e89ac92fb8703d584e83fac4d9eb5 > files > 7

pvs-sbcl-5.0-16.fc18.src.rpm

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

Perl :: Catalyst :: PostgreSQL :: RPM Valid HTML 4.01 Transitional