Attachment 37292 Details for Bug 59429 – file.shar

file.shar

file.shar (text/plain), 9.79 KB, created by Marc van Woerkom on 2003-11-18 18:40:09 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Marc van Woerkom

Created: 2003-11-18 18:40:09 UTC

Size: 9.79 KB

patch

obsolete

># This is a shell archive.  Save it in a file, remove anything before
># this line, and then unpack it by entering "sh file".  Note, it may
># create directories; files and directories will be owned by you and
># have default permissions.
>#
># This archive contains:
>#
>#	smv
>#	smv/distinfo
>#	smv/Makefile
>#	smv/pkg-descr
>#	smv/files
>#	smv/files/patch-bdd.c
>#	smv/files/patch-storage.c
>#	smv/files/patch-hash.c
>#	smv/files/patch-node.c
>#	smv/files/patch-makefile
>#	smv/files/patch-storage.h
>#	smv/files/patch-string.c
>#	smv/pkg-plist
>#
>echo c - smv
>mkdir -p smv > /dev/null 2>&1
>echo x - smv/distinfo
>sed 's/^X//' >smv/distinfo << 'END-of-smv/distinfo'
>XMD5 (smv.r2.5.4.3.tar.gz) = dd1a7ebcbac935845fc73eb8957386cb
>END-of-smv/distinfo
>echo x - smv/Makefile
>sed 's/^X//' >smv/Makefile << 'END-of-smv/Makefile'
>X# New ports collection makefile for: smv
>X# Date created: 18 November 2003
>X# Whom: Marc E.E. van Woerkom <marc.vanwoerkom@fernuni-hagen.de>
>X#
>X# $FreeBSD$
>X#
>X
>XPORTNAME=      smv
>XPORTVERSION=   2.5.4.3
>XCATEGORIES=    devel
>XMASTER_SITES=  http://www-2.cs.cmu.edu/~modelcheck/smv/
>XDISTNAME=      ${PORTNAME}.r${PORTVERSION}
>X
>XMAINTAINER=    marc.vanwoerkom@fernuni-hagen.de
>XCOMMENT=       A model checker
>X
>XWRKSRC=        ${WRKDIR}/smv
>XALL_TARGET=    smv
>X
>XMAN1=          smv.1
>X
>XMANCOMPRESSED=no
>X
>Xpost-patch:
>X	@${MV} ${WRKSRC}/makefile ${WRKSRC}/Makefile
>X
>Xdo-install:
>X	${INSTALL_PROGRAM} ${WRKSRC}/smv ${PREFIX}/bin
>X	${MKDIR} ${PREFIX}/share/smv
>X	${INSTALL_DATA} ${WRKSRC}/smv-mode.el ${DATADIR}
>X
>Xpost-install:
>X.if !defined(NOPORTDOCS)
>X	${INSTALL_MAN} ${WRKSRC}/smv.1 ${PREFIX}/man/man1
>X	${MKDIR} ${DOCSDIR}
>X	${INSTALL_MAN} ${WRKSRC}/NEW ${DOCSDIR}
>X	${INSTALL_MAN} ${WRKSRC}/README ${DOCSDIR}
>X	${INSTALL_MAN} ${WRKSRC}/doc/smvmanual.ps ${DOCSDIR}
>X	${MKDIR} ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/counter.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/dme1.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/dme2.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/featuring.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/gigamax.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/mutex.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/mutex1.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/periodic.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/ring.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/semaphore.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/short.smv ${EXAMPLESDIR}
>X	${INSTALL_MAN} ${WRKSRC}/examples/syncarb5.smv ${EXAMPLESDIR}
>X.endif
>X
>X.include <bsd.port.mk>
>END-of-smv/Makefile
>echo x - smv/pkg-descr
>sed 's/^X//' >smv/pkg-descr << 'END-of-smv/pkg-descr'
>XThe SMV (Symbolic Model Verifier) system is a tool for 
>Xchecking finite state systems against specifications 
>Xin the temporal logic CTL (Computational Tree Logic). 
>X
>XOne specifies the finite state system (finite automaton,
>XMealy machine, full adder circuit, ..) as a Kripke 
>Xstructure in the SMV language and provides specificaations 
>Xin CTL. The model checking algorithm allows to determine 
>Xif the Kripke structure fulfills the specifications.
>X
>XWWW: http://www-2.cs.cmu.edu/~modelcheck/smv.html
>X
>XMarc E.E. van Woerkom
>Xmarc.vanwoerkom@fernuni-hagen.de
>END-of-smv/pkg-descr
>echo c - smv/files
>mkdir -p smv/files > /dev/null 2>&1
>echo x - smv/files/patch-bdd.c
>sed 's/^X//' >smv/files/patch-bdd.c << 'END-of-smv/files/patch-bdd.c'
>X--- bdd.c
>X+++ bdd.c
>X@@ -113,7 +113,7 @@
>X    /* Initialize a keytable. */
>X    kp->n = n;
>X    kp->elements_in_table = 0;
>X-   kp->hash_table_buf = (bdd_ptr *)malloc(n*sizeof(bdd_ptr));
>X+   kp->hash_table_buf = (bdd_ptr *)smv_malloc(n*sizeof(bdd_ptr));
>X 
>X    {  /* Initialize hash bin list pointers to NULL. */
>X       register int i;
>X@@ -139,7 +139,7 @@
>X    /* Create key tables. */
>X    create_keytable(&reduce_table, KEYTABLESIZE);
>X    apply_cache_size = APPLY_CACHE_SIZE;
>X-   apply_cache = (apply_rec *)malloc(sizeof(apply_rec)*apply_cache_size);
>X+   apply_cache = (apply_rec *)smv_malloc(sizeof(apply_rec)*apply_cache_size);
>X    {
>X      int i;
>X      for(i=0;i<apply_cache_size;i++)apply_cache[i].op = 0;
>X@@ -1446,7 +1446,7 @@
>X }
>X 
>X /* An "infinity" constant - big enough power of 2 not to care about */
>X-#define INFINITY 1000
>X+#define SMV_INFINITY 1000
>X 
>X /* similar to auxcount_bdd, but computes log2 of the fraction */
>X 
>X@@ -1457,18 +1457,18 @@
>X   union {float a; bdd_ptr b;} temp;     /* very dangerous!!! */
>X   double l,r;
>X 
>X-  if(d==ZERO)return(-INFINITY); /* = log(0) */
>X+  if(d==ZERO)return(-SMV_INFINITY); /* = log(0) */
>X   if(d==ONE)return(0.0);        /* = log2(1) */
>X   temp.b = find_apply(COUNT_OP,d,ZERO);
>X   if(temp.b==NULL) {
>X     l = auxcount_bdd_log2(d->left,n);
>X     r = auxcount_bdd_log2(d->right,n);
>X     if(l < r) {
>X-      if(r - l > INFINITY) temp.a = r;
>X+      if(r - l > SMV_INFINITY) temp.a = r;
>X       else temp.a = l - 1.0 + log2(1.0 + pow(2.0,r-l));
>X     }
>X     else {
>X-      if(l - r > INFINITY) temp.a = l;
>X+      if(l - r > SMV_INFINITY) temp.a = l;
>X       else temp.a = r - 1.0 + log2(1.0 + pow(2.0,l-r));
>X     }
>X   }
>END-of-smv/files/patch-bdd.c
>echo x - smv/files/patch-storage.c
>sed 's/^X//' >smv/files/patch-storage.c << 'END-of-smv/files/patch-storage.c'
>X--- storage.c
>X+++ storage.c
>X@@ -9,7 +9,7 @@
>X {
>X #ifdef MACH
>X   mach_init();		/* needed to make sbrk() work */
>X-#endif MACH
>X+#endif
>X   /* addrfree points to the first free byte
>X      addrlimit points to the memory limit */
>X     addrfree = addrlimit = (char *) sbrk(0);
>X@@ -34,7 +34,7 @@
>X }
>X 
>X /* provide malloc for miscellaneuos storage allocation */
>X-char *malloc(n)
>X+char* smv_malloc(n)
>X int n;
>X {
>X   if(n % 4)n=n+4-(n%4);  /* always allocate multiple of four bytes */
>X@@ -47,7 +47,7 @@
>X }
>X 
>X /* very simple implementation of free */
>X-void free(p)
>X+void smv_free(p)
>X char *p;
>X {
>X   return;
>X@@ -61,7 +61,7 @@
>X mgr_ptr new_mgr(rec_size)
>X int rec_size;
>X {
>X-  register mgr_ptr mp = (mgr_ptr)malloc(sizeof(struct mgr));
>X+  register mgr_ptr mp = (mgr_ptr)smv_malloc(sizeof(struct mgr));
>X   mp->free.link = 0;
>X   mp->rec_size = rec_size;
>X   mp->count = 0;
>Xdiff -ru ./storage.h /usr3/marc/research/hagen/10-ws0304/77075 Model Checking/praktikum/smv/smv/storage.h
>END-of-smv/files/patch-storage.c
>echo x - smv/files/patch-hash.c
>sed 's/^X//' >smv/files/patch-hash.c << 'END-of-smv/files/patch-hash.c'
>X--- hash.c
>X+++ hash.c
>X@@ -7,12 +7,12 @@
>X int (*hash_fun)(),(*eq_fun)();
>X mgr_ptr mgr;
>X {
>X-  hash_ptr res = (hash_ptr)malloc(sizeof(struct hash));
>X+  hash_ptr res = (hash_ptr)smv_malloc(sizeof(struct hash));
>X   res->size = init_size;
>X   res->hash_fun = hash_fun;
>X   res->eq_fun = eq_fun;
>X   res->mgr = mgr;
>X-  res->tab = (rec_ptr *)malloc(init_size * sizeof(rec_ptr));
>X+  res->tab = (rec_ptr *)smv_malloc(init_size * sizeof(rec_ptr));
>X   bzero(res->tab,init_size * sizeof(rec_ptr));
>X   return(res);
>X }
>END-of-smv/files/patch-hash.c
>echo x - smv/files/patch-node.c
>sed 's/^X//' >smv/files/patch-node.c << 'END-of-smv/files/patch-node.c'
>X--- node.c
>X+++ node.c
>X@@ -609,7 +609,7 @@
>X node_ptr n;
>X int col;
>X {
>X-  char *buf = (char *)malloc(option_print_node_length + 1);
>X+  char *buf = (char *)smv_malloc(option_print_node_length + 1);
>X   int c,p;
>X   if(buf == NULL) rpterr("Out of memory");
>X   buf[0] = 0;
>X@@ -623,7 +623,7 @@
>X   }
>X   fprintf(stream,"%s",buf);
>X   if(!c)fprintf(stream,"...");
>X-  free(buf);
>X+  smv_free(buf);
>X   return(col + p);
>X }
>END-of-smv/files/patch-node.c
>echo x - smv/files/patch-makefile
>sed 's/^X//' >smv/files/patch-makefile << 'END-of-smv/files/patch-makefile'
>X--- makefile
>X+++ makefile
>X@@ -50,8 +50,8 @@
>X input.c: input.lex
>X 	$(LEX) $(LEXFLAGS) input.lex; mv lex.yy.c input.c
>X 
>X-# Recompile main.c if makefile changes.  This may be the change of version.
>X-main.o: main.c init.h makefile
>X+# Recompile main.c if Makefile changes.  This may be the change of version.
>X+main.o: main.c init.h Makefile
>X init.o: init.c init.h y.tab.h assoc.h  storage.h bdd.h hash.h node.h string.h
>X assoc.o: assoc.c assoc.h storage.h hash.h node.h
>X bdd.o: bdd.c assoc.h storage.h bdd.h hash.h node.h y.tab.h
>X@@ -66,7 +66,7 @@
>X clean:
>X 	rm -f *.o grammar.c grammar.y input.lex input.c y.tab.h
>X SRC= \
>X-  makefile \
>X+  Makefile \
>X   README \
>X   assoc.c \
>X   assoc.h \
>END-of-smv/files/patch-makefile
>echo x - smv/files/patch-storage.h
>sed 's/^X//' >smv/files/patch-storage.h << 'END-of-smv/files/patch-storage.h'
>X--- storage.h
>X+++ storage.h
>X@@ -12,8 +12,8 @@
>X #define ALLOCSIZE (2<<15)
>X 
>X void init_storage();
>X-char *malloc();
>X-void free();
>X+char* smv_malloc();
>X+void smv_free();
>X mgr_ptr new_mgr();
>X rec_ptr new_rec(),dup_rec();
>X void free_rec();
>END-of-smv/files/patch-storage.h
>echo x - smv/files/patch-string.c
>sed 's/^X//' >smv/files/patch-string.c << 'END-of-smv/files/patch-string.c'
>X--- string.c
>X+++ string.c
>X@@ -35,7 +35,7 @@
>X   string_rec a,*res;
>X   a.text = x;
>X   if(res = (string_ptr)find_hash(string_hash,&a))return(res);
>X-  a.text = (char *)strcpy((char *)malloc(strlen(x)+1),x);
>X+  a.text = (char *)strcpy((char *)smv_malloc(strlen(x)+1),x);
>X   return((string_ptr)insert_hash(string_hash,&a));
>X }
>END-of-smv/files/patch-string.c
>echo x - smv/pkg-plist
>sed 's/^X//' >smv/pkg-plist << 'END-of-smv/pkg-plist'
>Xbin/smv
>Xshare/smv/smv-mode.el
>X%%PORTDOCS%%%%DOCSDIR%%/NEW
>X%%PORTDOCS%%%%DOCSDIR%%/README
>X%%PORTDOCS%%%%DOCSDIR%%/smvmanual.ps
>X%%PORTDOCS%%%%EXAMPLESDIR%%/counter.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/dme1.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/dme2.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/featuring.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/gigamax.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/mutex.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/mutex1.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/periodic.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/ring.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/semaphore.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/short.smv
>X%%PORTDOCS%%%%EXAMPLESDIR%%/syncarb5.smv
>X%%PORTDOCS%%@dirrm %%DOCSDIR%%
>X%%PORTDOCS%%@dirrm %%EXAMPLESDIR%%
>X@dirrm share/smv
>END-of-smv/pkg-plist
>exit

Actions: View

Attachments on bug 59429: 37292