pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/devel/verifast
Module Name: pkgsrc
Committed By: ryoon
Date: Wed Jul 12 01:54:16 UTC 2017
Added Files:
pkgsrc/devel/verifast: DESCR Makefile PLIST distinfo
pkgsrc/devel/verifast/patches: patch-src_GNUmakefile
Log Message:
Import verifast-17.06 as devel/verifast.
VeriFast is a research prototype of a tool for modular formal
verification of correctness properties of single-threaded and
multithreaded C and Java programs annotated with preconditions and
postconditions written in separation logic.
This is recommended by Kiwamu Okabe in Japan NetBSD Users' Group BOF 2017
at the University of Tokyo.
To generate a diff of this commit:
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/verifast/DESCR \
pkgsrc/devel/verifast/Makefile pkgsrc/devel/verifast/PLIST \
pkgsrc/devel/verifast/distinfo
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/verifast/patches/patch-src_GNUmakefile
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Added files:
Index: pkgsrc/devel/verifast/DESCR
diff -u /dev/null pkgsrc/devel/verifast/DESCR:1.1
--- /dev/null Wed Jul 12 01:54:16 2017
+++ pkgsrc/devel/verifast/DESCR Wed Jul 12 01:54:16 2017
@@ -0,0 +1,4 @@
+VeriFast is a research prototype of a tool for modular formal
+verification of correctness properties of single-threaded and
+multithreaded C and Java programs annotated with preconditions and
+postconditions written in separation logic.
Index: pkgsrc/devel/verifast/Makefile
diff -u /dev/null pkgsrc/devel/verifast/Makefile:1.1
--- /dev/null Wed Jul 12 01:54:16 2017
+++ pkgsrc/devel/verifast/Makefile Wed Jul 12 01:54:16 2017
@@ -0,0 +1,36 @@
+# $NetBSD: Makefile,v 1.1 2017/07/12 01:54:16 ryoon Exp $
+
+DISTNAME= verifast-17.06
+CATEGORIES= devel
+MASTER_SITES= ${MASTER_SITE_GITHUB:=verifast/}
+GITHUB_PROJECT= verifast
+GITHUB_TAG= v${PKGVERSION_NOREV}
+
+MAINTAINER= ryoon%NetBSD.org@localhost
+HOMEPAGE= https://people.cs.kuleuven.be/~bart.jacobs/verifast/
+COMMENT= VeriFast code verifier in separation logic
+LICENSE= mit
+
+USE_TOOLS+= gmake pax pkg-config
+MAKE_FILE= GNUmakefile
+BUILD_MAKE_FLAGS+= -C src
+
+BUILD_DEPENDS+= vala-[0-9]*:../../lang/vala
+BUILD_DEPENDS+= camlp4-[0-9]*:../../lang/camlp4
+
+VF_DIR= share/verifast
+INSTALLATION_DIRS= ${VF_DIR} bin
+
+do-install:
+ cd ${WRKSRC}/bin && ${FIND} . -type f -print | \
+ pax -rw -pmp ${DESTDIR}${PREFIX}/${VF_DIR}
+ ${ECHO} "#! ${SH}" > ${DESTDIR}${PREFIX}/bin/vfide
+ ${ECHO} '${PREFIX}/${VF_DIR}/vfide "$$@"' \
+ >> ${DESTDIR}${PREFIX}/bin/vfide
+ ${CHMOD} 755 ${DESTDIR}${PREFIX}/bin/vfide
+
+.include "../../lang/camlp4/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml= full
+.include "../../lang/ocaml/buildlink3.mk"
+.include "../../x11/ocaml-lablgtk/buildlink3.mk"
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/devel/verifast/PLIST
diff -u /dev/null pkgsrc/devel/verifast/PLIST:1.1
--- /dev/null Wed Jul 12 01:54:16 2017
+++ pkgsrc/devel/verifast/PLIST Wed Jul 12 01:54:16 2017
@@ -0,0 +1,86 @@
+@comment $NetBSD: PLIST,v 1.1 2017/07/12 01:54:16 ryoon Exp $
+bin/vfide
+share/verifast/arpa/inet.h
+share/verifast/arrays.c
+share/verifast/arrays.gh
+share/verifast/arrays.vfmanifest
+share/verifast/assoclist.c
+share/verifast/assoclist.gh
+share/verifast/assoclist.vfmanifest
+share/verifast/assume.dll.vfmanifest
+share/verifast/bigstar.gh
+share/verifast/bigstar.vfmanifest
+share/verifast/bits/pthreadtypes.h
+share/verifast/counting.gh
+share/verifast/crt.dll.vfmanifest
+share/verifast/crt.vfmanifest
+share/verifast/dlsymtool
+share/verifast/ghost_cells.gh
+share/verifast/io.gh
+share/verifast/io.vfmanifest
+share/verifast/java_card_applet
+share/verifast/list.c
+share/verifast/list.gh
+share/verifast/list.vfmanifest
+share/verifast/listex.c
+share/verifast/listex.gh
+share/verifast/listex.vfmanifest
+share/verifast/lseg.gh
+share/verifast/main_class
+share/verifast/malloc.h
+share/verifast/maps.gh
+share/verifast/math.h
+share/verifast/mysh
+share/verifast/nat.gh
+share/verifast/permutations.c
+share/verifast/permutations.gh
+share/verifast/permutations.vfmanifest
+share/verifast/prelude.h
+share/verifast/prelude_core.gh
+share/verifast/pthread.h
+share/verifast/pthread.vfmanifest
+share/verifast/quantifiers.c
+share/verifast/quantifiers.gh
+share/verifast/quantifiers.vfmanifest
+share/verifast/raw_ghost_lists.c
+share/verifast/raw_ghost_lists.gh
+share/verifast/raw_ghost_lists.vfmanifest
+share/verifast/rt/_assume.javaspec
+share/verifast/rt/_atomics.javaspec
+share/verifast/rt/_bitops.javaspec
+share/verifast/rt/_list.java
+share/verifast/rt/_list.javaspec
+share/verifast/rt/_nat.javaspec
+share/verifast/rt/_quantifiers.javaspec
+share/verifast/rt/java.io.javaspec
+share/verifast/rt/java.lang.javaspec
+share/verifast/rt/java.lang_verified.javaspec
+share/verifast/rt/java.net.javaspec
+share/verifast/rt/java.nio.channels.javaspec
+share/verifast/rt/java.nio.javaspec
+share/verifast/rt/java.util.concurrent.javaspec
+share/verifast/rt/java.util.javaspec
+share/verifast/rt/javacard.framework.javaspec
+share/verifast/rt/javacard.security.javaspec
+share/verifast/rt/javacardx.crypto.javaspec
+share/verifast/rt/org.globalplatform.javaspec
+share/verifast/rt/rt.jarspec
+share/verifast/rt/rt_verified.jarspec
+share/verifast/rt/rt_verified.jarsrc
+share/verifast/stdbool.h
+share/verifast/stddef.h
+share/verifast/stdint.h
+share/verifast/stdio.h
+share/verifast/stdio_simple.h
+share/verifast/stdio_simple.vfmanifest
+share/verifast/stdlib.h
+share/verifast/string.h
+share/verifast/threading.c
+share/verifast/threading.h
+share/verifast/threading.vfmanifest
+share/verifast/unistd.h
+share/verifast/verifast
+share/verifast/vf__floating_point.h
+share/verifast/vfide
+share/verifast/vfidedemo.bat
+share/verifast/vfstrip
Index: pkgsrc/devel/verifast/distinfo
diff -u /dev/null pkgsrc/devel/verifast/distinfo:1.1
--- /dev/null Wed Jul 12 01:54:16 2017
+++ pkgsrc/devel/verifast/distinfo Wed Jul 12 01:54:16 2017
@@ -0,0 +1,7 @@
+$NetBSD: distinfo,v 1.1 2017/07/12 01:54:16 ryoon Exp $
+
+SHA1 (verifast-17.06.tar.gz) = 9c918c6fa88ab11315fe80abfa097dcc8d0f85cd
+RMD160 (verifast-17.06.tar.gz) = 8808173823c6697272450ba0eac71cfc4824af54
+SHA512 (verifast-17.06.tar.gz) = f4ffe75cf5d47e48f565c34b12dd134f6ffd527a12146484f8cf14549b0e5292c8e4b4e077fe1c8ae93c0f045ba8760e42369ddaea2b47fef9f37e0403202193
+Size (verifast-17.06.tar.gz) = 1698045 bytes
+SHA1 (patch-src_GNUmakefile) = ceb2071c030d6120e6c25b497deba75fcf53d8ba
Index: pkgsrc/devel/verifast/patches/patch-src_GNUmakefile
diff -u /dev/null pkgsrc/devel/verifast/patches/patch-src_GNUmakefile:1.1
--- /dev/null Wed Jul 12 01:54:16 2017
+++ pkgsrc/devel/verifast/patches/patch-src_GNUmakefile Wed Jul 12 01:54:16 2017
@@ -0,0 +1,75 @@
+$NetBSD: patch-src_GNUmakefile,v 1.1 2017/07/12 01:54:16 ryoon Exp $
+
+* Fix build under NetBSD
+
+--- src/GNUmakefile.orig 2017-06-13 16:58:54.000000000 +0000
++++ src/GNUmakefile
+@@ -41,6 +41,8 @@ else
+ OS = Darwin
+ else ifeq ($(shell uname -o), Cygwin)
+ OS = Cygwin
++ else ifeq ($(shell uname -s), NetBSD)
++ OS = NetBSD
+ else
+ $(error "Could not recognize your platform")
+ endif
+@@ -50,6 +52,9 @@ endif
+ ifndef WITHOUT_LABLGTK
+ ifeq ($(OS), Cygwin)
+ LABLGTK_FLAGS += -I +site-lib/lablgtk2 lablgtk.cmxa
++ else ifeq ($(OS), NetBSD)
++ LABLGTK_FLAGS_ += -I +site-lib/lablgtk2
++ LABLGTK_FLAGS += ${LABLGTK_FLAGS_} lablgtk.cmxa
+ else
+ LABLGTK_FLAGS_ += -I +../lablgtk2 -I +lablgtk2
+ LABLGTK_FLAGS += ${LABLGTK_FLAGS_} lablgtk.cmxa
+@@ -137,11 +142,7 @@ OCAML = ${OCAMLBIN}/ocaml
+ OCAMLC = $(firstword $(wildcard ${OCAMLBIN}/ocamlc.opt ${OCAMLBIN}/ocamlc))
+ OCAMLOPT = $(firstword $(wildcard ${OCAMLBIN}/ocamlopt.opt ${OCAMLBIN}/ocamlopt))
+ OCAMLDEP = $(firstword $(wildcard ${OCAMLBIN}/ocamldep.opt ${OCAMLBIN}/ocamldep))
+-ifeq ($(OS), Cygwin)
+- CAMLP4O = camlp4o.opt
+-else
+- CAMLP4O = $(firstword $(wildcard ${OCAMLBIN}/camlp4o.opt ${OCAMLBIN}/camlp4o))
+-endif
++CAMLP4O = camlp4o.opt
+
+ # Do we build with "-I ./linux" or "-I ./win":
+ ifeq ($(OS), Cygwin)
+@@ -198,6 +199,9 @@ endif
+ ifeq ($(OS), Cygwin)
+ include win/GNUmakefile
+ endif
++ifeq ($(OS), NetBSD)
++ include linux/GNUmakefile
++endif
+
+ include java_frontend/GNUmakefile
+
+@@ -378,7 +382,7 @@ clean::
+ ifndef WITHOUT_LABLGTK
+
+ clean::
+- cd linemarks; make clean
++ cd linemarks; ${MAKE} clean
+
+ branchleft_png.ml: branch-left.png
+ gdk_pixbuf_mlsource branch-left.png > branchleft_png.ml
+@@ -396,7 +400,7 @@ branchright_png.cmx: branchright_png.ml
+ vfide.cmx: branchleft_png.cmx branchright_png.cmx Fonts.cmx vfide.ml $(GTKSOURCEVIEW_DEPS)
+ @echo " OCAMLOPT " $@
+ ifndef WITHOUT_GTKSOURCEVIEW
+- make -C linemarks OCAMLOPT=${OCAMLOPT} OCAMLCFLAGS="${OCAMLCFLAGS}" LABLGTK_FLAGS="$(LABLGTK_FLAGS_)" linemarks.cmxa
++ ${MAKE} -C linemarks OCAMLOPT=${OCAMLOPT} OCAMLCFLAGS="${OCAMLCFLAGS}" LABLGTK_FLAGS="$(LABLGTK_FLAGS_)" linemarks.cmxa
+ endif
+ $(SET_LDD); $(OCAMLOPT) $(OCAMLCFLAGS) -thread -c -w p -warn-error FSU -c $(INCLUDES) \
+ -pp ${CAMLP4O} nums.cmxa $(LABLGTK_FLAGS) $(GTKSOURCEVIEW_LFLAGS) vfide.ml
+@@ -404,7 +408,7 @@ endif
+ ../bin/vfide$(DOTEXE): vfide.cmx redux.cmx $(Z3DEPS) plugins2.cmx $(GTKSOURCEVIEW_DEPS)
+ @echo " OCAMLOPT " $@
+ ifndef WITHOUT_GTKSOURCEVIEW
+- cd linemarks; make linemarks.cmxa
++ cd linemarks; ${MAKE} linemarks.cmxa
+ endif
+ $(SET_LDD); ${OCAMLOPT} $(OCAMLCFLAGS) -warn-error F -pp ${CAMLP4O} -o ../bin/vfide$(DOTEXE) \
+ $(LABLGTK_FLAGS) $(GTKSOURCEVIEW_LFLAGS) unix.cmxa \
Home |
Main Index |
Thread Index |
Old Index