INSTALL.md 15.5 KB
Newer Older
1
2
3
4
5
6
# Installing Frama-C

- [Installing Frama-C](#installing-frama-c)
    - [Table of Contents](#table-of-contents)
    - [Installing Frama-C via opam](#installing-frama-c-via-opam)
        - [Installing opam](#installing-opam)
7
8
9
        - [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository)
        - [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)
        - [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl)
10
        - [Installing Frama-C on macOS](#installing-frama-c-on-macos)
11
12
13
14
    - [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora)
    - [Compiling from source](#compiling-from-source)
        - [Quick Start](#quick-start)
        - [Full Compilation Guide](#full-compilation-guide)
15
- [Testing the Installation](#testing-the-installation)
16
17
18
19
20
21
22
    - [Available resources](#available-resources)
        - [Executables: (in `/INSTALL_DIR/bin`)](#executables-in-install_dirbin)
        - [Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)](#shared-files-in-install_dirshareframa-c-and-subdirectories)
        - [Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)](#documentation-files-in-install_dirshareframa-cdoc)
        - [Object files: (in `/INSTALL_DIR/lib/frama-c`)](#object-files-in-install_dirlibframa-c)
        - [Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)](#plugin-files-in-install_dirlibframa-cplugins)
        - [Man files: (in `/INSTALL_DIR/man/man1`)](#man-files-in-install_dirmanman1)
23
- [Installing Additional Frama-C Plugins](#installing-additional-frama-c-plugins)
24
    - [HAVE FUN WITH FRAMA-C!](#have-fun-with-frama-c)
25
26
27
28
29
30

## Installing Frama-C via opam

[opam](http://opam.ocaml.org/) is the OCaml package manager. Every Frama-C
release is made available via an opam package.

31
First you need to install opam, then you may install Frama-C using opam.
32
33
34
35
36

### Installing opam

Several Linux distributions already include an `opam` package.

37
**Note:** make sure your opam version is >= 2.0.0.
38

39
40
41
macOS has opam through Homebrew.

Windows users can install opam via WSL (Windows Subsystem for Linux).
42

43
If your system does not have an opam package >= 2.0.0, you can
44
[compile it from source](#compiling-from-source),
45
46
47
48
or use the provided opam binaries available at:

http://opam.ocaml.org/doc/Install.html

49
### Installing Frama-C from opam repository
50
51
52
53

The Frama-C package in opam is called `frama-c`, which includes both the
command-line `frama-c` executable and the graphical interface `frama-c-gui`.

54
`frama-c` has some non-OCaml dependencies, such as Gtk and GMP. In most
55
56
57
systems, opam can take care of these external dependencies through
its `depext` plug-in: issuing the two commands

58
    # install Frama-C's dependencies
59
60
61
62
63
64
65
66
67
    opam install depext
    opam depext frama-c

will install the appropriate system packages (this of course requires
administrator rights on the system).

If your system is not supported by `depext`, you will need to install
Gtk, GtkSourceView, GnomeCanvas and GMP, including development libraries,
separately. If you do so, please consider providing the system name and list of
68
packages (e.g. via a [Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new))
69
70
so that we can add it to the Frama-C `depext` package.

71
72
73
    # install Frama-C
    opam install frama-c

74
75
### Configuring provers for Frama-C/WP

76
77
Frama-C/WP uses the [Why3](http://why3.lri.fr/) platform to run external provers
for proving ACSL annotations.
78
The Why3 platform and the Alt-Ergo prover are automatically installed _via_ opam
79
80
when installing Frama-C.

81
82
Other recommended, efficient provers are CVC4 and Z3.
They can be used as replacement or combined with Alt-Ergo.
83
Actually, you can use any prover supported by Why3 in combination with Frama-C/WP.
84

85
86
Most provers are available on all platforms. After their installation,
Why3 must be configured to make them available for Frama-C/WP:
87

88
89
90
```shell
why3 config --detect
```
91

92
### Reference configuration
93

94
See file [reference-configuration.md](reference-configuration.md)
95
for a set of packages that is known to work with Frama-C 22 (Titanium).
96

97
### Installing Custom Versions of Frama-C
98
99
100
101
102
103
104

If you have a **non-standard** version of Frama-C available
(with proprietary extensions, custom plugins, etc.),
you can use opam to install Frama-C's dependencies and compile your
own sources directly:

    # optional: remove the standard frama-c package if it was installed
105
    opam remove --force frama-c
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

    # install Frama-C's dependencies
    opam install depext
    opam depext frama-c
    opam install --deps-only frama-c

    # install custom version of frama-c
    opam pin add --kind=path frama-c <dir>

where `<dir>` is the root of your unpacked Frama-C archive.
See `opam pin` for more details.

If your extensions require other libraries than the ones already used
by Frama-C, they must of course be installed as well.

121
### Installing Frama-C on Windows via WSL
122

123
124
Frama-C is developed on Linux, but it can be installed on Windows using the
following tools:
125

126
- Windows Subsystem for Linux
127
- VcXsrv (X server for Windows)
128

129
130
131
#### Prerequisites: WSL + a Linux distribution

For enabling WSL on Windows, you may follow these instructions
132
(we tested with Ubuntu 20.04 LTS;
133
134
other distributions/versions should also work,
but the instructions below may require some modifications).
135

136
https://docs.microsoft.com/en-us/windows/wsl/install-win10
137

138
139
140
141
142
143
144
145
146
147
148
Note: older builds of Windows 10 and systems without access to the
      Microsoft Store may have no compatible Linux packages.

##### PowerShell-based quick guide

This is a quick guide based on running a PowerShell with administrator rights.
Note that, depending on your build version of Windows 10, the Ubuntu package
selected below may not work. If you are unsure, follow the above instructions
from the Microsoft website.

Inside PowerShell, run the following command to activate Windows Subsystem for Linux:
149

150
151
152
```
Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux
```
153

154
155
156
157
Then, reboot the operating system.

After rebooting, run again the PowerShell terminal with administrator rights.
Move to your user directory, download the distribution and install it:
158
159
160

```
cd C:\Users\<Your User Directory>
161
Invoke-WebRequest -Uri https://aka.ms/wslubuntu2004 -OutFile Ubuntu.appx -UseBasicParsing
162
163
164
165
166
167
Add-AppxPackage .\Ubuntu.appx
```

Ubuntu should now be available in the Windows menu. Run it and follow the
instructions to create a user.

168
169
#### Installing opam and Frama-C on WSL

170
171
172
173
174
175
For installing opam, some packages are required. The following commands can be
run to update the system and install those packages:

```
sudo apt update
sudo apt upgrade
176
sudo apt install make m4 gcc opam yaru-theme-gtk yaru-theme-icon
177
178
179
180
181
```

Then opam can be set up using these commands:

```
182
opam init --disable-sandboxing --shell-setup
183
184
185
186
187
188
189
190
191
192
193
194
eval $(opam env)
opam install -y depext
```

Now, for installing Frama-C, run the following commands that will use `apt` to
install the dependencies of the opam packages and then install them:

```
opam depext --install -y lablgtk3 lablgtk3-sourceview3
opam depext --install -y frama-c
```

195
196
#### Running the Frama-C GUI on WSL

197
198
199
Microsoft WSL does not support graphical user interfaces directly. If you want
to run Frama-C's GUI, you need to install an X server, such as VcXsrv or
Cygwin/X. We present below how to install VcXsrv.
200

201
First, install VcXsrv from:
202

203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
https://sourceforge.net/projects/vcxsrv/

The default installation settings should work.
Now run it from the Windows menu (it is named XLaunch).
On the first configuration screen, select "Multiple Windows". On the
second, keep "Start no client" selected. On the third configuration step, add an
additional parameter `-nocursor` in the field "Additional parameters for
VcXsrv". You can save this configuration at the last step if you want, before
clicking "Finish".

Once it is done, the Xserver is ready. From WSL, run:

```
export DISPLAY=:0
frama-c-gui
```
219
220
221
222
223

### Installing Frama-C on macOS

[opam](https://opam.ocaml.org) works perfectly on macOS via
[Homebrew](https://brew.sh).
224
We highly recommend to rely on it for the installation of Frama-C.
225
226
227
228
229
230
231
232

1. Install *required* general macOS tools for OCaml:

    ```shell
    brew install autoconf pkg-config opam
    ```

   Do not forget to `opam init` and ``eval `opam config env` `` for a proper
233
   opam installation (if not already done before).
234

235
236
237
238
239
240
241
242
2. Set up a compatible OCaml version (replace `<version>` with the version
   indicated in the 'recommended working configuration' section):

    ```shell
    opam switch create <version>
    ```

3. Install *required* dependencies for Frama-C:
243
244
245
246
247

    ```shell
    brew install gmp gtk+ gtksourceview libgnomecanvas
    ```

Loïc Correnson's avatar
Loïc Correnson committed
248
    The graphical libraries require additional manual configuration of your
249
250
251
252
    bash profile. Consult this [issue](https://github.com/ocaml/opam-repository/issues/13709) on opam
    for details. A known working configuration is:

    ```shell
Loïc Correnson's avatar
Loïc Correnson committed
253
    export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig
254
255
    ```

256
4. Install *recommended* dependencies for Frama-C:
257
258
259
260
261

    ```shell
    brew install graphviz
    ```

262
5. Install Frama-C:
263
264

    ```shell
265
    opam install frama-c
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
    ```

## Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)

**NOTE**: Distribution packages are updated later than opam packages,
          so if you want access to the most recent versions of Frama-C,
          opam is currently the recommended approach.

Also note that it is **not** recommended to mix OCaml packages installed by
your distribution with packages installed via opam. When using opam,
we recommend uninstalling all `ocaml-*` packages from your distribution, and
then installing, exclusively via opam, an OCaml compiler and all the OCaml
packages you need. This ensures that only those versions will be in the PATH.

The advantage of using distribution packages is that dependencies are almost
always handled by the distribution's package manager. The disadvantage is that,
if you need some optional OCaml package that has not been packaged in your
distribution (e.g. `landmarks`, which is distributed via opam), it may be very
hard to install it, since mixing opam and non-opam packages often fails
(and is **strongly** discouraged).

Debian/Ubuntu: `apt-get install frama-c`

Fedora: `dnf install frama-c`

291
Arch Linux: `pikaur -S frama-c`
292
293
294
295
296
297
298
299

## Compiling from source

**Note**: These instructions are no longer required in the vast majority
          of cases. They are kept here mostly for historical reference.

### Quick Start

300
301
1. Install [opam](http://opam.ocaml.org/) and use it to get all of Frama-C's
   dependencies (including some external ones):
302

303
304
305
        opam install depext
        opam depext frama-c
        opam install --deps-only frama-c
306

307
308
309
310
311
312
313
314
   If not using [opam](http://opam.ocaml.org/), you will need to install
   the Frama-C dependencies by yourself. The `opam/opam` file in the Frama-C
   .tar.gz lists the required dependencies (e.g. `ocamlfind`, `ocamlgraph`,
   `zarith`, etc.). A few of these dependencies are optional, only required
   for the graphical interface: `lablgtk`, `conf-gnomecanvas` and
   `conf-gtksourceview` (or the equivalent Gtk+3 packages).

2. On Linux-like distributions:
315
316
317
318
319

        ./configure && make && sudo make install

    See section *Configuration* below for options.

320
3. On Windows+Cygwin:
321
322
323

        ./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install

324
4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
325
326
327
328
329

### Full Compilation Guide

#### Frama-C Requirements

330
331
332
See the `opam/opam` file, section `depends`, for compatible OCaml versions and
required dependencies (except for those related to `lablgtk`, which are
required for the GUI but otherwise optional).
333

334
Section `deptops` lists optional dependencies.
335
336
337
338
339
340
341
342
343

#### Configuration

Frama-C 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`.

A plugin can be enabled by `--enable-plugin` and disabled by `--disable-plugin`.
344
345
By default, all distributed plugins are enabled, unless some optional
dependencies are not met.
346
347
348
349
350
351
352
353
354
355
356
357

See `./configure --help` for the current list of plugins, and available options.

##### Under Cygwin

Use `./configure --prefix="$(cygpath -a -m <installation path>)"`.

(using Unix-style paths without the drive letter will probably not work)


#### Compilation

358
Type `make` (you can use `-j` for parallelization).
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385

Some Makefile targets of interest are:
- `doc`      generates the API documentation.
- `oracles`  sets up the Frama-C test suite oracles for your own configuration.
- `tests`    performs Frama-C's own tests.


#### Installation

Type `make install`
(depending on the installation directory, this may require superuser
privileges. The installation directory is chosen through `--prefix`).


#### API Documentation

For plugin developers, the API documentation of the Frama-C kernel and
distributed plugins is available in the file `frama-c-api.tar.gz`, after running
`make doc-distrib`.


#### Uninstallation

Type `make uninstall` to remove Frama-C and all the installed plugins.
(Depending on the installation directory, this may require superuser
privileges.)

386

387
388
389
390
391
392
# Testing the Installation

This step is optional.

Download some test files:

393
    export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
    wget -P test ${PREFIX_URL}/CruiseControl.c
    wget -P test ${PREFIX_URL}/CruiseControl_const.c
    wget -P test ${PREFIX_URL}/CruiseControl.h
    wget -P test ${PREFIX_URL}/CruiseControl_extern.h
    wget -P test ${PREFIX_URL}/scade_types.h
    wget -P test ${PREFIX_URL}/config_types.h
    wget -P test ${PREFIX_URL}/definitions.h

Then test your installation by running:

    frama-c -eva test/CruiseControl*.c
    # or (if frama-c-gui is available)
    frama-c-gui -eva test/CruiseControl*.c

# Available resources
409
410
411
412

Once Frama-C is installed, the following resources should be installed and
available:

413
## Executables: (in `/INSTALL_DIR/bin`)
414
415
416
417
418
419
420

- `frama-c`
- `frama-c-gui`       if available
- `frama-c-config`    displays Frama-C configuration paths
- `frama-c.byte`      bytecode version of frama-c
- `frama-c-gui.byte`  bytecode version of frama-c-gui, if available
- `ptests.opt`        testing tool for Frama-c
421
- `frama-c-script`    utilities related to analysis parametrization
422

423
## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
424
425
426
427
428
429
430

- some `.h` and `.c` files used as preludes by Frama-C
- some `Makefiles` used to compile dynamic plugins
- some `.rc` files used to configure Frama-C
- some image files used by the Frama-C GUI
- some files for Frama-C/plug-in development (autocomplete scripts,
  Emacs settings, scripts for running Eva, ...)
431
432
- an annotated C standard library (with ACSL annotations) in `libc`
- plugin-specific files (in directories `wp`, `e-acsl`, etc.)
433

434
## Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)
435
436
437

- files used to generate dynamic plugin documentation

438
## Object files: (in `/INSTALL_DIR/lib/frama-c`)
439
440
441

- object files used to compile dynamic plugins

442
## Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)
443
444
445

- object files of available dynamic plugins

446
## Man files: (in `/INSTALL_DIR/share/man/man1`)
447
448
449
450

- `man` files for `frama-c` (and `frama-c-gui` if available)


451
# Installing Additional Frama-C Plugins
452
453
454
455
456
457
458
459
460
461
462

Plugins may be released independently of Frama-C.

The standard way for installing them should be:

    ./configure && make && make install

Plugins may have their own custom installation procedures.
Consult their specific documentation for details.


463
# HAVE FUN WITH FRAMA-C!