From f88ce312327e7663589bf34876c649386cd87596 Mon Sep 17 00:00:00 2001
From: Frama-CI Bot <frama-ci-bot@frama-c.com>
Date: Thu, 26 Oct 2023 16:02:03 +0000
Subject: [PATCH] [release] prepare 28.0~beta-nickel
On behalf of "Andre Maroneze" <andre.maroneze@cea.fr> (@maroneze)
---
_events/framac-28.0-beta.md | 35 ++
_fc-versions/nickel.md | 44 ++
download/acsl-1.20.pdf | 3 +
.../acsl-implementation-28.0-beta-Nickel.pdf | 3 +
.../aorai-example-28.0-beta-Nickel.tar.gz | 3 +
download/aorai-manual-28.0-beta-Nickel.pdf | 3 +
download/e-acsl/e-acsl-1.19.pdf | 4 +-
...e-acsl-implementation-28.0-beta-Nickel.pdf | 3 +
.../e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf | 3 +
download/eva-manual-28.0-beta-Nickel.pdf | 3 +
download/frama-c-28.0-beta-Nickel-api.tar.gz | 3 +
download/frama-c-28.0-beta-Nickel.tar.gz | 3 +
...frama-c-server-28.0-beta-Nickel-api.tar.gz | 3 +
download/hello-28.0-beta-Nickel.tar.gz | 3 +
download/metrics-manual-28.0-beta-Nickel.pdf | 3 +
...gin-development-guide-28.0-beta-Nickel.pdf | 3 +
download/rte-manual-28.0-beta-Nickel.pdf | 3 +
download/user-manual-28.0-beta-Nickel.pdf | 3 +
download/wp-manual-28.0-beta-Nickel.pdf | 3 +
html/installations/nickel.md | 532 ++++++++++++++++++
20 files changed, 661 insertions(+), 2 deletions(-)
create mode 100644 _events/framac-28.0-beta.md
create mode 100644 _fc-versions/nickel.md
create mode 100644 download/acsl-1.20.pdf
create mode 100644 download/acsl-implementation-28.0-beta-Nickel.pdf
create mode 100644 download/aorai-example-28.0-beta-Nickel.tar.gz
create mode 100644 download/aorai-manual-28.0-beta-Nickel.pdf
create mode 100644 download/e-acsl/e-acsl-implementation-28.0-beta-Nickel.pdf
create mode 100644 download/e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf
create mode 100644 download/eva-manual-28.0-beta-Nickel.pdf
create mode 100644 download/frama-c-28.0-beta-Nickel-api.tar.gz
create mode 100644 download/frama-c-28.0-beta-Nickel.tar.gz
create mode 100644 download/frama-c-server-28.0-beta-Nickel-api.tar.gz
create mode 100644 download/hello-28.0-beta-Nickel.tar.gz
create mode 100644 download/metrics-manual-28.0-beta-Nickel.pdf
create mode 100644 download/plugin-development-guide-28.0-beta-Nickel.pdf
create mode 100644 download/rte-manual-28.0-beta-Nickel.pdf
create mode 100644 download/user-manual-28.0-beta-Nickel.pdf
create mode 100644 download/wp-manual-28.0-beta-Nickel.pdf
create mode 100644 html/installations/nickel.md
diff --git a/_events/framac-28.0-beta.md b/_events/framac-28.0-beta.md
new file mode 100644
index 00000000..5a15d7a0
--- /dev/null
+++ b/_events/framac-28.0-beta.md
@@ -0,0 +1,35 @@
+---
+layout: default
+date: "26-10-2023"
+short_title: Frama-C 28.0~beta (Nickel)
+title: Beta release of Frama-C 28.0~beta (Nickel)
+link: /fc-versions/nickel.html
+---
+
+Frama-C 28.0~beta (Nickel) is out. Download it [here](/fc-versions/nickel.html).
+
+Main changes with respect to Frama-C 27.0 (Cobalt) include:
+
+#### Kernel
+- Frama-C can now generate more default clauses (in particular terminates and exits)
+- Removed deprecated options `-no-type` and `-no-obj`
+
+#### Alias
+- New plugin Alias, implements a points-to analysis
+
+#### E-ACSL
+- More efficient code arithmetic calculations
+
+#### Eva
+- Support for simple `\let` bindings
+- Removed deprecated Db.Value API
+- Fixed unsoundness about initialization with goto and switch
+
+#### WP
+- New ACSL extensions for defining automatic proof strategies
+- WP generates default exits and terminates, removed old options `-wp-*-terminate`
+- Fixed cache for interactive provers
+
+#### Ivette
+- Basic component for WP
+- Many bug fixes
diff --git a/_fc-versions/nickel.md b/_fc-versions/nickel.md
new file mode 100644
index 00000000..788b9abc
--- /dev/null
+++ b/_fc-versions/nickel.md
@@ -0,0 +1,44 @@
+---
+layout: version
+number: 28
+name: Nickel
+beta: true
+releases:
+- number: 0
+ categories:
+ - name: Frama-C v28.0~beta Nickel
+ files:
+ - name: Source distribution
+ link: /download/frama-c-28.0-beta-Nickel.tar.gz
+ help: Compilation instructions
+ help_link: /html/installations/nickel.html
+ - name: User manual
+ link: /download/user-manual-28.0-beta-Nickel.pdf
+ - name: Plug-in development guide
+ link: /download/plugin-development-guide-28.0-beta-Nickel.pdf
+ help: Hello plug-in tutorial archive
+ help_link: /download/hello-28.0-beta-Nickel.tar.gz
+ - name: API Documentation
+ link: /download/frama-c-28.0-beta-Nickel-api.tar.gz
+ - name: Server API Documentation
+ link: /download/frama-c-server-28.0-beta-Nickel-api.tar.gz
+ - name: ACSL 1.20 (Nickel implementation)
+ link: /download/acsl-implementation-28.0-beta-Nickel.pdf
+ - name: Plug-in Manuals
+ sort: true
+ files:
+ - name: Aoraï manual
+ link: /download/aorai-manual-28.0-beta-Nickel.pdf
+ help: Aoraï example
+ help_link: /download/aorai-example-28.0-beta-Nickel.tar.gz
+ - name: Metrics manual
+ link: /download/metrics-manual-28.0-beta-Nickel.pdf
+ - name: Rte manual
+ link: /download/rte-manual-28.0-beta-Nickel.pdf
+ - name: Eva manual
+ link: /download/eva-manual-28.0-beta-Nickel.pdf
+ - name: WP manual
+ link: /download/wp-manual-28.0-beta-Nickel.pdf
+ - name: E-ACSL manual
+ link: /download/e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf
+---
diff --git a/download/acsl-1.20.pdf b/download/acsl-1.20.pdf
new file mode 100644
index 00000000..26407a8c
--- /dev/null
+++ b/download/acsl-1.20.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:40a81f744d0e8e42733b115e5948ce2ac831a2b3dcc813a27f2924db7d2664a6
+size 2028114
diff --git a/download/acsl-implementation-28.0-beta-Nickel.pdf b/download/acsl-implementation-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..a16d2538
--- /dev/null
+++ b/download/acsl-implementation-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:b44807df706a759d4eeb0e252662aee46c890c2e6d2f4a7dc6cdd95120d65036
+size 2033183
diff --git a/download/aorai-example-28.0-beta-Nickel.tar.gz b/download/aorai-example-28.0-beta-Nickel.tar.gz
new file mode 100644
index 00000000..3c80cda1
--- /dev/null
+++ b/download/aorai-example-28.0-beta-Nickel.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:a1d7e40ab249a649263267df43d16237bb7ba0176f15d842adf9d99ef66aa126
+size 1279
diff --git a/download/aorai-manual-28.0-beta-Nickel.pdf b/download/aorai-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..654e2996
--- /dev/null
+++ b/download/aorai-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:0cc5bf36fbd7a0ce6d9b7a218a425b71f506cce8e8365317f839ba11e03d02f3
+size 1332704
diff --git a/download/e-acsl/e-acsl-1.19.pdf b/download/e-acsl/e-acsl-1.19.pdf
index 1945b2af..1ce05ef5 100644
--- a/download/e-acsl/e-acsl-1.19.pdf
+++ b/download/e-acsl/e-acsl-1.19.pdf
@@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
-oid sha256:d2ebf58199a2d20d1c9947249ca4540367702e6c9868946005eb9fb01b22a4a4
-size 1271968
+oid sha256:18e5ffb49173b01ca466f3c96a92495006bb0abf7c7ddb706667b59f7517b54e
+size 1271965
diff --git a/download/e-acsl/e-acsl-implementation-28.0-beta-Nickel.pdf b/download/e-acsl/e-acsl-implementation-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..1c388fc6
--- /dev/null
+++ b/download/e-acsl/e-acsl-implementation-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:8f3bf8402f420eb53651c4023e782de64e23c1ea9651d7ebbaaa61a0c374313f
+size 1329753
diff --git a/download/e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf b/download/e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..ef99dc4d
--- /dev/null
+++ b/download/e-acsl/e-acsl-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:bc3880f07bb58153bd9c975e098a517441796f14c27a549439cea931c5fa1133
+size 1370303
diff --git a/download/eva-manual-28.0-beta-Nickel.pdf b/download/eva-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..b1cdc189
--- /dev/null
+++ b/download/eva-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:1b4decbefc2910297e749a11822616039bbe82d79e06fd468da8d88c789e6610
+size 2555774
diff --git a/download/frama-c-28.0-beta-Nickel-api.tar.gz b/download/frama-c-28.0-beta-Nickel-api.tar.gz
new file mode 100644
index 00000000..b37be516
--- /dev/null
+++ b/download/frama-c-28.0-beta-Nickel-api.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:8f830c20845f2d7ddef4cf951a2b8bc71dbfb810ebb96c72982ec421412905fd
+size 4694850
diff --git a/download/frama-c-28.0-beta-Nickel.tar.gz b/download/frama-c-28.0-beta-Nickel.tar.gz
new file mode 100644
index 00000000..ec7acad7
--- /dev/null
+++ b/download/frama-c-28.0-beta-Nickel.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:0c80dae8074fcb3f6a33d7a41faf9939a2a336478a8d2c79e20e2d7bab953735
+size 8068829
diff --git a/download/frama-c-server-28.0-beta-Nickel-api.tar.gz b/download/frama-c-server-28.0-beta-Nickel-api.tar.gz
new file mode 100644
index 00000000..c4e55681
--- /dev/null
+++ b/download/frama-c-server-28.0-beta-Nickel-api.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:d30e2f6f109103daaa7e29fea5047dd166f58e81b330af39933f8690488f9510
+size 40635
diff --git a/download/hello-28.0-beta-Nickel.tar.gz b/download/hello-28.0-beta-Nickel.tar.gz
new file mode 100644
index 00000000..1ef1ca4c
--- /dev/null
+++ b/download/hello-28.0-beta-Nickel.tar.gz
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:f61f27bd17de546264aa58f40f3aafaac7021e0ef69c17f6b1b4cd7664a037ec
+size 20
diff --git a/download/metrics-manual-28.0-beta-Nickel.pdf b/download/metrics-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..4f9e5115
--- /dev/null
+++ b/download/metrics-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:e42ec8302275a3c91924dbde5f0e810f48b81e09972773eddc13ccdcd7067c34
+size 1394593
diff --git a/download/plugin-development-guide-28.0-beta-Nickel.pdf b/download/plugin-development-guide-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..db24e809
--- /dev/null
+++ b/download/plugin-development-guide-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:123d8d2bbd878c198c7ac82e128c4e236c4b28de89e483193618a7698ac08768
+size 1973005
diff --git a/download/rte-manual-28.0-beta-Nickel.pdf b/download/rte-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..4a5b04a4
--- /dev/null
+++ b/download/rte-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:d08a2026ffc324aae0288dbd413e0caec08672bf4fa2d04fa7f054122fab649d
+size 1285296
diff --git a/download/user-manual-28.0-beta-Nickel.pdf b/download/user-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..c8933d7c
--- /dev/null
+++ b/download/user-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:b07176a2b2247602e8f2ca648466b286b357da68a3755f4ad150b478837df5e6
+size 2460333
diff --git a/download/wp-manual-28.0-beta-Nickel.pdf b/download/wp-manual-28.0-beta-Nickel.pdf
new file mode 100644
index 00000000..989b92d7
--- /dev/null
+++ b/download/wp-manual-28.0-beta-Nickel.pdf
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:dfb47cff4eb7173d8917d95c3e51394a48654adf53b647a819626789ddbbdd66
+size 1896114
diff --git a/html/installations/nickel.md b/html/installations/nickel.md
new file mode 100644
index 00000000..0cfa9342
--- /dev/null
+++ b/html/installations/nickel.md
@@ -0,0 +1,532 @@
+---
+layout: installation_page
+version: nickel
+title: Installation instructions for Frama-C 28.0~beta (Nickel)
+---
+# Installing Frama-C (released on 2023-10-26)
+
+- [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)
+ - [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)
+ - [Installing Frama-C on macOS](#installing-frama-c-on-macos)
+ - [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)
+- [Testing the Installation](#testing-the-installation)
+ - [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/share/man/man1`)](#man-files-in-install_dirsharemanman1)
+- [Installing Additional Frama-C Plugins](#installing-additional-frama-c-plugins)
+- [Frama-C additional tools](#frama-c-additional-tools)
+ - [HAVE FUN WITH FRAMA-C!](#have-fun-with-frama-c)
+
+## 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.
+
+First you need to install opam, then you may install Frama-C using opam.
+
+### Installing opam
+
+Several Linux distributions already include an `opam` package.
+
+macOS has opam through Homebrew.
+
+Windows users can install opam via WSL (Windows Subsystem for Linux).
+
+If your system does not have an opam package >= 2, you can use the provided
+opam binaries available at:
+
+http://opam.ocaml.org/doc/Install.html
+
+### Installing Frama-C from opam repository
+
+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`.
+
+`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)
+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 explicitly with the following commands, before
+installing Frama-C as above. Again, installing the external dependencies
+requires administrative rights.
+
+ # install Frama-C's dependencies with pre-2.1.0 opam
+ opam install depext
+ opam depext frama-c
+
+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.
+
+### Configuring provers for Frama-C/WP
+
+Frama-C/WP uses the [Why3](http://why3.lri.fr/) platform to run external provers
+for proving ACSL annotations.
+The Why3 platform and the Alt-Ergo prover are automatically installed _via_ opam
+when installing Frama-C.
+
+Other recommended, efficient provers are CVC4 and Z3.
+They can be used as replacement or combined with Alt-Ergo.
+Actually, you can use any prover supported by Why3 in combination with Frama-C/WP.
+
+Most provers are available on all platforms. After their installation,
+Why3 must be configured to make them available for Frama-C/WP:
+
+```shell
+why3 config detect
+```
+
+### Reference configuration
+
+See file [reference-configuration.md](reference-configuration.md)
+for a set of packages that is known to work with this version of Frama-C.
+
+### Installing Custom Versions of Frama-C
+
+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
+ opam remove --force frama-c
+
+ # install Frama-C's dependencies
+ opam install depext # only for opam < 2.1.0
+ opam depext frama-c # only for opam < 2.1.0
+ opam install --deps-only frama-c [--with-test]
+
+ # 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. The option `--with-test` is optional and
+is necessary only if you want to be able to execute the tests available in
+the frama-c repository.
+
+If your extensions require other libraries than the ones already used
+by Frama-C, they must of course be installed as well.
+
+### Installing Frama-C on Windows via WSL
+
+Frama-C is developed on Linux, but it can be installed on Windows using the
+Windows Subsystem for Linux (WSL).
+
+**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").
+
+#### Prerequisites: WSL + a Linux distribution
+
+To enable WSL on Windows, you may follow these instructions
+(we tested with Ubuntu 20.04 LTS;
+other distributions/versions should also work,
+but the instructions below may require some modifications).
+
+https://docs.microsoft.com/en-us/windows/wsl/install
+
+Notes:
+
+- 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**.
+
+#### Installing opam and Frama-C on WSL
+
+To install 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
+sudo apt install make m4 gcc opam gnome-icon-theme
+```
+
+Then opam can be set up using these commands:
+
+```
+opam init --disable-sandboxing --shell-setup
+eval $(opam env)
+opam install -y depext
+```
+
+You can force a particular Ocaml version during `opam init` by using the option
+`-c <version>` if needed. For instance, you can try installing the OCaml version
+mentioned in the [reference configuration](reference-configuration.md).
+
+Now, to install Frama-C, run the following commands, which 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
+```
+
+#### Running the Frama-C GUI on WSL
+
+If you have WSL2: a known issue with some versions of Frama-C, lablgtk3 and
+Wayland requires 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.
+
+First, install VcXsrv from:
+
+https://sourceforge.net/projects/vcxsrv/
+
+The default installation settings should work.
+
+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".
+
+Now specific settings must be provided in WSL. you can put the export commands
+in your `~/.bashrc` file, so this is done automatically when starting WSL.
+
+##### WSL 1
+
+The Xserver is ready. From WSL, run:
+
+```
+export LIBGL_ALWAYS_INDIRECT=1
+export DISPLAY=:0
+frama-c-gui
+```
+
+##### WSL 2
+
+```
+export LIBGL_ALWAYS_INDIRECT=1
+export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.0
+frama-c-gui
+```
+
+### Installing Frama-C on macOS
+
+[opam](https://opam.ocaml.org) works perfectly on macOS via
+[Homebrew](https://brew.sh).
+We highly recommend to rely on it for the installation of Frama-C.
+
+1. Install *required* general macOS tools for OCaml:
+
+ ```shell
+ brew install opam
+ ```
+
+ Do not forget to `opam init` and `eval $(opam env)` for a proper
+ opam installation (if not already done before).
+
+2. Set up a compatible OCaml version (replace `<version>` with the version
+ indicated in the [reference configuration](#reference-configuration)):
+
+ ```shell
+ opam switch create <version>
+ ```
+
+3. Install Frama-C:
+
+ ```shell
+ opam install frama-c
+ ```
+
+ Opam may ask for the administrator password to handle required system
+ dependencies.
+
+ **It is likely that, at this point, opam will fail due to some Homebrew
+ packages and pkg-config.** The error messages should indicate what you need
+ to do, e.g.:
+
+ ```shell
+ For pkg-config to find zlib you may need to set:
+ export PKG_CONFIG_PATH="/usr/local/opt/zlib/lib/pkgconfig"
+ ```
+
+ After setting such environment variables, re-running `opam install frama-c`
+ should work. If you still have issues, try manually installing the required
+ packages (via `brew install <package>`) and then re-installing Frama-C.
+ **Note**: opam packages prefixed with `conf-` only check if the
+ corresponding system package is findable. If you cannot install some
+ `conf-` package, the solution will likely involve Homebrew and/or setting
+ environment variables, not opam.
+
+4. Install the new Frama-C graphical interface (Ivette).
+
+ **The traditional GTK-based Frama-C GUI no longer works on macOS!**
+
+ You need to use Ivette, the new Frama-C graphical interface.
+ Instructions on installing and running it are presented by opam when
+ the `frama-c` package is installed. Follow them to get Ivette running.
+
+
+## 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`
+
+Arch Linux: `pikaur -S frama-c`
+
+## 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
+
+1. Install [opam](http://opam.ocaml.org/) and use it to get all of Frama-C's
+ dependencies (including some external ones):
+
+ opam install depext # only for opam < 2.1.0
+ opam depext frama-c # only for opam < 2.1.0
+ opam install --deps-only frama-c
+
+ If not using [opam](http://opam.ocaml.org/), you will need to install
+ the Frama-C dependencies by yourself. The `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:
+
+ make RELEASE=yes && make install
+
+ See section *Installation* below for options.
+
+3. On Windows+Cygwin:
+
+ make RELEASE=yes && make install
+
+4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
+
+### Full Compilation Guide
+
+#### Frama-C Requirements
+
+See the `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).
+
+To install the required dependencies, you can use opam v2.1
+or higher to do the following (assuming you are in frama-c
+root source folder):
+
+1. `opam switch create frama-c ocaml-base-compiler.4.13.1`
+ to create a compatible opam switch
+1. `opam pin . -n` to pin to the latest development version
+1. `opam install --deps-only .` will fetch and build all
+ relevant dependencies
+
+#### Compilation
+
+There are basically two compilation modes: development and release.
+
+Typing `make` builds in development mode, this is a shortcut for:
+```
+dune build @install
+```
+
+Typing `make RELEASE=yes` builds in release mode, this is a shortcut for:
+```
+dune build @install --release --promote-install-files=false
+```
+
+For more precise build configuration, use directly the `dune` command.
+
+#### Testing
+
+Basic tests can be executed using:
+
+```
+make run-ptests
+make default-tests
+```
+
+**Beware!** If the tests fail due to JSON output, it is likely because of the
+Yojson package version. Make sure that your `opam` dependencies have been
+installed with the option `--with-test`
+(see [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)).
+
+#### Installation
+
+Type `make install` (depending on the installation directory, this may require
+superuser privileges. The installation directory is chosen through the variable
+`PREFIX`). This is a shortcut for:
+
+```
+dune install
+```
+
+The Makefile (and dune) supports the `DESTDIR` variable, that can be used to
+configure the location of the installation.
+
+#### API Documentation
+
+For plugin developers, the API documentation of the Frama-C kernel and
+distributed plugins is available in the `_build/default/_doc/_html` directory
+after running:
+
+```
+make doc
+```
+
+or:
+
+```
+dune build @doc
+```
+
+#### Uninstallation
+
+Type `make uninstall` to remove Frama-C and all the installed plugins.
+(Depending on the installation directory, this may require superuser
+privileges.)
+
+
+# Testing the Installation
+
+This step is optional.
+
+Download some test files:
+
+ export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
+ 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
+
+Once Frama-C is installed, the following resources should be installed and
+available:
+
+## Executables: (in `/INSTALL_DIR/bin`)
+
+- `frama-c`
+- `frama-c-gui` if available
+- `frama-c-config` lightweight wrapper used to display configuration paths
+- `frama-c-hdrck` header checking tool for Frama-C
+- `frama-c-ptests` testing tool for Frama-c
+- `frama-c-wtests` testing tool for Frama-c
+- `frama-c-script` utilities related to analysis parametrization
+
+## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
+
+- 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, ...)
+- an annotated C standard library (with ACSL annotations) in `libc`
+- plugin-specific files (in directories `wp`, `e-acsl`, etc.)
+
+## Object files: (in `/INSTALL_DIR/lib/frama-c`)
+
+- object files used to compile dynamic plugins
+
+## Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)
+
+- object files of available dynamic plugins
+
+## Man files: (in `/INSTALL_DIR/share/man/man1`)
+
+- `man` files for `frama-c` (and `frama-c-gui` if available)
+
+
+# Installing Additional Frama-C Plugins
+
+Plugins may be released independently of Frama-C.
+
+The standard way for installing them should be:
+
+ dune build @install && dune install
+
+Plugins may have their own custom installation procedures.
+Consult their specific documentation for details.
+
+# Frama-C additional tools
+
+A few additional tools that are unnecessary for most users might be useful for
+plugin developers. These tools are:
+- `frama-c-lint`, used for checking coding conventions
+- `frama-c-hdrck`, used for checking file license headers
+
+They can be installed either by pinning them via Opam:
+
+```
+opam pin tools/lint
+opam pin tools/hdrck
+```
+
+Or by compiling/installing Frama-C manually in developer mode:
+```
+FRAMAC_DEVELOPER=yes make
+FRAMAC_DEVELOPER=yes make install
+
+# Or:
+make -C tools/<the-tool>
+make -C tools/<the-tool> install
+```
+
+For convenience, `FRAMAC_DEVELOPER` can be exported globally.
+
+
+# HAVE FUN WITH FRAMA-C!
--
GitLab