pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
[pkgsrc/trunk]: pkgsrc/devel/verifast Import verifast-17.06 as devel/verifast.
details: https://anonhg.NetBSD.org/pkgsrc/rev/9ed10ad70306
branches: trunk
changeset: 365242:9ed10ad70306
user: ryoon <ryoon%pkgsrc.org@localhost>
date: Wed Jul 12 01:54:16 2017 +0000
description:
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.
diffstat:
devel/verifast/DESCR | 4 +
devel/verifast/Makefile | 36 +++++++++++
devel/verifast/PLIST | 86 ++++++++++++++++++++++++++++
devel/verifast/distinfo | 7 ++
devel/verifast/patches/patch-src_GNUmakefile | 75 ++++++++++++++++++++++++
5 files changed, 208 insertions(+), 0 deletions(-)
diffs (228 lines):
diff -r 5737da1963d7 -r 9ed10ad70306 devel/verifast/DESCR
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/verifast/DESCR Wed Jul 12 01:54:16 2017 +0000
@@ -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.
diff -r 5737da1963d7 -r 9ed10ad70306 devel/verifast/Makefile
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/verifast/Makefile Wed Jul 12 01:54:16 2017 +0000
@@ -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"
diff -r 5737da1963d7 -r 9ed10ad70306 devel/verifast/PLIST
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/verifast/PLIST Wed Jul 12 01:54:16 2017 +0000
@@ -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
diff -r 5737da1963d7 -r 9ed10ad70306 devel/verifast/distinfo
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/verifast/distinfo Wed Jul 12 01:54:16 2017 +0000
@@ -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
diff -r 5737da1963d7 -r 9ed10ad70306 devel/verifast/patches/patch-src_GNUmakefile
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/devel/verifast/patches/patch-src_GNUmakefile Wed Jul 12 01:54:16 2017 +0000
@@ -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