./devel/verifast, VeriFast code verifier in separation logic

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: CURRENT, Version: 17.06nb2, Package name: verifast-17.06nb2, Maintainer: ryoon

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.


Required to run:
[lang/ocaml] [lang/camlp4] [x11/ocaml-lablgtk]

Required to build:
[pkgtools/x11-links] [x11/compositeproto] [x11/glproto] [x11/renderproto] [x11/xproto] [x11/xf86vidmodeproto] [x11/recordproto] [x11/xf86driproto] [x11/damageproto] [x11/inputproto] [x11/xextproto] [x11/randrproto] [x11/dri2proto] [lang/vala] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [lang/camlp4]

Master sites:

SHA1: 9c918c6fa88ab11315fe80abfa097dcc8d0f85cd
RMD160: 8808173823c6697272450ba0eac71cfc4824af54
Filesize: 1658.247 KB

Version history: (Expand)


CVS history: (Expand)


   2017-09-18 11:53:40 by Maya Rashish | Files touched by this commit (676)
Log message:
revbump for requiring ICU 59.x
   2017-09-09 23:57:46 by David A. Holland | Files touched by this commit (3)
Log message:
Don't randomly use the implementation namespace. Fixes clang build.

Also, pass MAKE_JOBS as the number of CPUs to use when testing, as
otherwise it gets 0 and apparently interprets that as "infinitely
many".

XXX: The test suite should not really be run as part of the build.
   2017-09-08 11:51:27 by Jaap Boender | Files touched by this commit (113) | Package updated
Log message:
Recursive revbump associated with update of ocaml to 4.05
   2017-07-12 03:54:16 by Ryo ONODERA | Files touched by this commit (5)
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.