-
Notifications
You must be signed in to change notification settings - Fork 3
/
README
76 lines (50 loc) · 2.32 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
The jStar Verifier
==================
jStar is a highly-customisable automatic verification tool based on separation
logic aiming at object-oriented programs written in Java.
There is a tutorial for the tool here:
./doc/tutorial/jstartut.pdf
For more information, see http://www.jstarverifier.org
Building on *nix / Mac OSX
---------------------------
Use the standard incantation.
./configure --prefix DIR
make install
(NOTE: In some environments, such as Mac OS Leopard, dynlink.cmxa is
unavailable, leading to a compile error. In that case, try "make install.byte".)
Assuming that DIR/bin is in your path, you should now be able to run jStar.
jstar
Optionally, run the tests to see that all is OK.
make test
Dependencies:
* OCaml >=3.11
http://caml.inria.fr/download.en.html
Debian / Ubuntu: ocaml, ocaml-native-compilers
Building on Win32
-----------------
Open the Visual Studio Command Prompt.
- If you obtained Microsoft tools not as a part of Visual Studio, just open
Command Prompt and manually set up necessary PATH and INCLUDE directories.)
Check that the make tool is in path.
- If using Cywgin/MinGW based make, then just add Cygwin/MinGW bin directory
to path. In addition, set the LIB environment variable to empty. This is
due to problems that arise when make deals with directories containing
empty spaces (like "Program Files"). You will probably have to manually set
up additional include path for OCaml compiler to Visual C++ Runtime
Libraries and Windows SDK libraries.
To run the build process, call:
make build
To set the environment variables necessary for jStar to run:
setjstarenv.bat
After the build process has finished, you may have to add extension .exe to
compiled binaries located in jStar's bin subdirectory.
Dependencies:
* Microsoft-based native Win32 port of OCaml:
http://caml.inria.fr/pub/distrib/ocaml-3.11/ocaml-3.11.0-win-msvc.exe
* FlexDLL: http://alain.frisch.fr/flexdll.html
(solves the problem that Windows DLL cannot refer to symbols defined
in the main application or in previously loaded DLLs)
* Microsoft Macro Assembler (ml.exe), Microsoft Visual C++ and
Microsoft Windows SDK libraries. (if you are not using Visual Studio,
these tools can be obtained for free at Microsoft site)
* Unix make tool (e.g., the one distributed with Cygwin or MinGW)