Newer
Older
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
-------------------------
INSTALLATION INSTRUCTIONS
-------------------------
===============================================================================
SUMMARY
===============================================================================
0) Summary
1) Quick Start
2) Requirements
3) Configuration
4) Compilation
5) Installation
6) Custom Installation
7) Testing the Installation
8) Uninstallation
9) Have Fun with E-ACSL!
===============================================================================
QUICK START
===============================================================================
1) Install Frama-C if not already installed.
2a) On Linux-like distribution:
./configure && make && sudo make install
2b) On Windows+Cygwin or Windows+MinGW+msys:
./configure --prefix C:/windows/path/with/direct/slash && make && make install
4) Optionally, test your installation by running:
frama-c.byte -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
frama-c -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
See below for more detailed and specific instructions.
===============================================================================
REQUIREMENTS
===============================================================================
- GNU make version >= 3.81
(no warranty that this plug-in works with a more recent version of Frama-C)
- The native version of the plug-in is only available if native dynamic linking
feature of OCaml is available on your system (see Frama-C User Manual,
Section 3.1).
- Optionally, the GMP library >= 4.3
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
It is required to run the tests and to run the generated programs,
but not to run the plug-in through Frama-C.
===============================================================================
CONFIGURATION
===============================================================================
The E-ACSL plug-in is configured by "./configure [options]"
configure is generated by autoconf, so that the standard options for setting
installation directories are available, in particular '--prefix=/path'.
Under Cygwin or MinGW:
----------------------
Use "./configure --prefix C:/windows/path/with/direct/slash".
===============================================================================
COMPILATION
===============================================================================
Type "make".
Makefile targets of interest are:
- doc generates the API documentation
===============================================================================
INSTALLATION
===============================================================================
Type "make install"
(depending on the installation directory, may require superuser privileges).
It is possible to install in a given directory by setting
the DESTDIR variable: "make install DESTDIR=/tmp" installs Frama-C in
sub-directories of /tmp.
The following files are installed.
Object files: (usually in `frama-c -print-plugin-path`)
-------------
- E_ACSL.cmi
- E_ACSL.cmo
- E_ACSL.cmxs (only if native dynamic linking of OCaml is available)
Shared files: (usually in `frama-c -print-share-path`/e-acsl)
-------------
- e_acsl_gmp.h
- e_acsl_gmp_types.h
- memory_model/e_acsl_bittree.[ch]
- memory_model/e_acsl_mmodel.[ch]
- memory_model/e_acsl_mmodel_api.[h]
Manuals: (usually in `frama-c -print-share-path`/manuals)
--------
- e-acsl.pdf
- e-acsl-implementation.pdf
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
===============================================================================
CUSTOM INSTALLATION
===============================================================================
You can manually move any installed files. However, in such a case, you have to
set specific environment variables in order that Frama-C found the appropriate
objects when required.
The environment variables are:
------------------------------
FRAMAC_SHARE: absolute path to the Frama-C share subdirectory
FRAMAC_LIB: absolute path of the Frama-C lib subdirectory
FRAMAC_PLUGIN: absolute path of the Frama-C plug-in directory.
===============================================================================
TESTING THE INSTALLATION
===============================================================================
This step is optional.
Test your installation by running:
frama-c.byte -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
frama-c -e-acsl tests/e-acsl-runtime/true.i -then-on e-acsl -print
The second command only works if native dynamic linking of OCaml is available
on your system.
===============================================================================
UNINSTALLATION
===============================================================================
Type "make uninstall" to remove Frama-C and all the installed plug-ins.
That works only if you have not manually moved the installed files (see Section
"Custom Installation").
===============================================================================
HAVE FUN WITH E-ACSL!
===============================================================================