I cloned the NASA PVS Library and configured my environment to use it, but I still get that same problem. Does the solution possibly rely on the very latest PVS from GitHub as well?
I am using 6.0, and have just cloned the PVS repository itself, as long as SBCL, but got stuck:
- I did figure out that I needed to run autoconf
- I also then figured out that my PVSPATH variable needs to end with a trailing “/“
- building SBCL depended on having SBCL (or another LISP) already built
I’ll eventually figure out how to build PVS, but just thought I’d let you know that with the default 6.0 PVS and the GitHub NASA libraries the problem persisted for me (on Mac OS X, if that’s relevant).
On Jul 10, 2015, at 9:58 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:
This theory type-checks without problem using the patches in the github
version of the NASA PVS Library. Sam recently added the attached patch,
which may have solved the problem.
Cesar A. Munoz NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx Bldg. 1220 Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446 Fax: +1 (757) 864 4234
On 7/10/15 3:31 AM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
on behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
真(p_しません: bool): bool =
しません(p_偽: bool): bool =