-
Notifications
You must be signed in to change notification settings - Fork 4
/
README.install.source
125 lines (82 loc) · 3.82 KB
/
README.install.source
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
*********************************
* KeY Source Code Installation *
* Version 1.5.x *
* Nightly Builds *
* (Development Version) *
********************************
(1) Requirements:
-------------------------------------
Operating System: Linux/Unix, MacOSX, Windows (untested)
Java 2 SDK, Version 1.5.x or newer (already installed)
Needed additional Libraries:
antlr.jar Version >= 2.7.2: parser generator
javacc.jar Version >= 3.0 : parser generator
recoderKey.jar
a transformation framework for java patched by the KeY group
junit.jar version 3.8.1: test framework
log4j.jar
Optionally, KeY can make use of the following binaries:
ESC Java's decision procedure 'Simplify'
SMT-LIB provers: bindings exist currently for Yices, CVCLite, CVC3 and SVC
(export to SMT input file possible)
(2) Contents of the KeY-Distribution
-------------------------------------
At the KeY-Homepage you can find the following parts:
* README.xxx-src.txt: this file
* KeY-xxx-src.tgz: the source code version of KeY-system
* KeYExtLib_xxx.tgz: contains the external libraries
* quicktour_xxx.ps.gz: a short tutorial
* KeYDemo_xxx.tgz: example for KeY used in the tutorial
(3) Installation (Source Code)
-------------------------------------
1) Untar the tar-gzipped file:
tar -xvzf KeY-xxx-src.tgz
2) Change to the created directory key-xxx
cd key-xxx
3) Install the needed libraries. Use the environment variable
$KEY_LIB to point to the directory the needed libraries are
in. If you use csh and all the needed libraries are in
~/key_lib use, e.g.
setenv KEY_LIB ~/key_lib
or (bash) export KEY_LIB=~/key_lib
or (Windows) set KEY_LIB=<path to libraries>
4) Optional: Install Simplify and/or SMT-LIB provers.
If you download Simplify not from the KeY-website but
elsewhere (e.g. as part of ESC/Java), follow the intallation
instructions given there. Then rename the Simplify binary which
could be named something like Simplify Simplify-1.5.4.linux
(Linux version) or Simplify-1.5.4.exe (Windows) to just 'Simplify'
resp. 'Simplify.exe'. When using Linux make sure that the file is
is executable (you can make a file executable by issuing the
command 'chmod a+x filename').
Make sure that the path where the binaries reside is included in
your PATH environment variable or in the KEY_LIB environment
variable. If not, use (e.g., in the csh to include Simplify
which is assumed to be located in ~/simplify):
setenv PATH ~/simplify:$PATH
In bash-syntax the above command is
export PATH=$PATH:~/simplify
(analog procedure for SMT-LIB provers)
5) Change to the subdirectory ./system
cd system
6) Compile KeY:
make all (or gmake all)
or
export ANT_OPTS="-Xmx512m"
ant
(compilation via 'ant' should work under Windows too, but you need to set the ANT_OPTS
environment variable most likely via
set ANT_OPTS = "-Xmx512m"
)
(4) Start KeY
-------------------------------
Assuming you are still in the 'system' directory, run:
../bin/runProver
(5) Start KeY in Test Generation Mode
-------------------------------------
Run 'startProver unit' or if you wish a simpler GUI run 'startProver testing'
(Windows: 'startProver.bat unit' or 'startProver.bat testing')
The library objenesis.jar may be required to run the generated tests.
-------------------------------
If you encounter problems, please send a message to
support@key-project.org