INSTALL.md 16.1 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
    - [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)
Allan Blanchard's avatar
Allan Blanchard committed
22
        - [Man files: (in `/INSTALL_DIR/share/man/man1`)](#man-files-in-install_dirsharemanman1)
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
38
39
macOS has opam through Homebrew.

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

41
42
If your system does not have an opam package >= 2, you can use the provided
opam binaries available at:
43
44
45

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

46
### Installing Frama-C from opam repository
47
48
49
50

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

51
52
53
54
`frama-c` has some non-OCaml dependencies, such as Gtk and GMP. On most
systems, `opam`'s `depext` mechanism can take care of installing these
external dependencies. As of version
2.1.0, `depext` is [directly included](https://opam.ocaml.org/blog/opam-2-1-0/#Seamless-integration-of-System-dependencies-handling-a-k-a-quot-depexts-quot)
55
56
57
58
59
60
61
62
63
64
in `opam`, so that the following command should install everything, at
least if your OS is supported by `depext` (and you have administrative
rights):

    opam install frama-c

For older `opam` versions, you have to install it
separately and call it explicitely with the following commands, before
installing Frama-C as above. Again, installing the external dependencies
requires administrative rights.
65
66

    # install Frama-C's dependencies with pre-2.1.0 opam
67
68
69
    opam install depext
    opam depext frama-c

70
71
72
73
74
75
If there are errors due to missing external dependencies, opam may emit a
message indicating which packages to install. If this is not sufficient,
there may be missing dependencies in opam's `depext` tool. In this case,
you may [create a Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new)
indicating your distribution and error message.

76
77
### Configuring provers for Frama-C/WP

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

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

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

90
```shell
91
why3 config detect
92
```
93

94
### Reference configuration
95

96
See file [reference-configuration.md](reference-configuration.md)
97
for a set of packages that is known to work with Frama-C 24 (Chromium).
98

99
### Installing Custom Versions of Frama-C
100
101
102
103
104
105
106

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
107
    opam remove --force frama-c
108
109

    # install Frama-C's dependencies
110
111
    opam install depext # only for opam < 2.1.0
    opam depext frama-c # only for opam < 2.1.0
112
113
114
115
116
117
118
119
120
121
122
    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.

123
### Installing Frama-C on Windows via WSL
124

125
Frama-C is developed on Linux, but it can be installed on Windows using the
126
Windows Subsystem for Linux (WSL).
127

128
129
130
131
**Note**: if you have WSL2 (Windows 11), you can run the graphical interface
          directly, thanks to WSLg. If you are using WSL 1, you need to install
          an X server for Windows, such as VcXsrv
          (see section "Running the Frama-C GUI on WSL").
132

133
134
#### Prerequisites: WSL + a Linux distribution

135
To enable WSL on Windows, you may follow these instructions
136
(we tested with Ubuntu 20.04 LTS;
137
138
other distributions/versions should also work,
but the instructions below may require some modifications).
139

140
https://docs.microsoft.com/en-us/windows/wsl/install
141

142
Notes:
143

144
145
146
147
- older builds of Windows 10 and systems without access to the
  Microsoft Store may have no compatible Linux packages.
- in WSL 1, Frama-C/WP cannot use Why3 because of some missing features in WSL
  support, thus using WSL 2 is **highly recommended**.
148

149
150
#### Installing opam and Frama-C on WSL

151
To install opam, some packages are required. The following commands can be
152
153
154
155
156
run to update the system and install those packages:

```
sudo apt update
sudo apt upgrade
157
sudo apt install make m4 gcc opam gnome-icon-theme
158
159
160
161
162
```

Then opam can be set up using these commands:

```
163
opam init --disable-sandboxing --shell-setup
164
165
166
167
eval $(opam env)
opam install -y depext
```

168
You can force a particular Ocaml version during `opam init` by using the option
169
170
`-c <version>` if needed. For instance, you can try installing the OCaml version
mentioned in the [reference configuration](reference-configuration.md).
171

172
Now, to install Frama-C, run the following commands, which will use `apt` to
173
174
175
176
177
178
179
install the dependencies of the opam packages and then install them:

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

180
181
#### Running the Frama-C GUI on WSL

182
183
184
185
186
187
188
189
190
If you have WSL2: a known issue with Frama-C 24.0 (Chromium), lablgtk3 and
Wayland require prefixing the command running the Frama-C GUI with
`GDK_BACKEND=x11`, as in:

    GDK_BACKEND=x11 frama-c-gui <options>

If you have WSL 1: WSL 1 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.
191

192
First, install VcXsrv from:
193

194
195
196
197
https://sourceforge.net/projects/vcxsrv/

The default installation settings should work.

198
199
200
201
202
203
204
205
Now run VcXsrv from the Windows menu (it is named XLaunch), the firewall
must authorize both "Public" and "Private" domains. On the first configuration
screen, select "Multiple Windows". On the second:

- keep "Start no client" selected,
- keep "Native opengl" selected,
- select "Disable access control".

206
Now specific settings must be provided in WSL. you can put the export commands
207
208
209
210
211
in your `~/.bashrc` file, so this is done automatically when starting WSL.

##### WSL 1

The Xserver is ready. From WSL, run:
212
213

```
214
export LIBGL_ALWAYS_INDIRECT=1
215
216
217
export DISPLAY=:0
frama-c-gui
```
218

219
220
221
222
223
224
225
226
##### WSL 2

```
export LIBGL_ALWAYS_INDIRECT=1
export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.0
frama-c-gui
```

227
228
229
230
### Installing Frama-C on macOS

[opam](https://opam.ocaml.org) works perfectly on macOS via
[Homebrew](https://brew.sh).
231
We highly recommend to rely on it for the installation of Frama-C.
232
233
234
235
236
237
238
239

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
240
   opam installation (if not already done before).
241

242
243
244
245
246
247
248
249
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:
250
251
252
253
254

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

Loïc Correnson's avatar
Loïc Correnson committed
255
    The graphical libraries require additional manual configuration of your
256
257
258
259
    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
260
    export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig
261
262
    ```

263
4. Install *recommended* dependencies for Frama-C:
264
265
266
267
268

    ```shell
    brew install graphviz
    ```

269
5. Install Frama-C:
270
271

    ```shell
272
    opam install frama-c
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
    ```

## 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`

298
Arch Linux: `pikaur -S frama-c`
299
300
301
302
303
304
305
306

## 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

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

310
311
        opam install depext # only for opam < 2.1.0
        opam depext frama-c # only for opam < 2.1.0
312
        opam install --deps-only frama-c
313

314
315
316
317
318
319
320
321
   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:
322
323
324
325
326

        ./configure && make && sudo make install

    See section *Configuration* below for options.

327
3. On Windows+Cygwin:
328
329
330

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

331
4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
332
333
334
335
336

### Full Compilation Guide

#### Frama-C Requirements

337
338
339
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).
340

Virgile Prevosto's avatar
typo    
Virgile Prevosto committed
341
Section `depopts` lists optional dependencies.
342
343
344
345
346
347
348
349
350

#### 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`.
351
352
By default, all distributed plugins are enabled, unless some optional
dependencies are not met.
353
354
355
356
357
358
359
360
361
362
363
364

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

365
Type `make` (you can use `-j` for parallelization).
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392

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.)

393

394
395
396
397
398
399
# Testing the Installation

This step is optional.

Download some test files:

400
    export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
    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
416
417
418
419

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

420
## Executables: (in `/INSTALL_DIR/bin`)
421
422
423

- `frama-c`
- `frama-c-gui`       if available
424
- `frama-c-config`    lightweight wrapper used to display configuration paths
425
426
427
- `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
428
- `frama-c-script`    utilities related to analysis parametrization
429

430
## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
431
432
433
434
435
436
437

- 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, ...)
438
439
- an annotated C standard library (with ACSL annotations) in `libc`
- plugin-specific files (in directories `wp`, `e-acsl`, etc.)
440

441
## Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)
442
443
444

- files used to generate dynamic plugin documentation

445
## Object files: (in `/INSTALL_DIR/lib/frama-c`)
446
447
448

- object files used to compile dynamic plugins

449
## Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)
450
451
452

- object files of available dynamic plugins

453
## Man files: (in `/INSTALL_DIR/share/man/man1`)
454
455
456
457

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


458
# Installing Additional Frama-C Plugins
459
460
461
462
463
464
465
466
467
468
469

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.


470
# HAVE FUN WITH FRAMA-C!