Author: github.com/Costava
Date: 2022 February
Manjaro version: Qonos 21.2.3 with Xfce
NOTE: If you want to do a "clean reinstall":
pamac remove opam ocaml ocaml-compiler-libs- Delete
.opamdirectory and.why3.conffrom your home directory. - Also delete
.why3.conf.bakif present in home directory. - Delete the "opam configuration" line from your
~/.bash_profile
For installing Frama-C, refer to:
https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md
and install via opam.
In short:
$ pamac install opam
$ opam init
$ opam install frama-cBe aware that after each of the second and third steps above, you will be given command(s) to run MANUALLY.
The instructions currently at:
https://www.frama-c.com/html/get-frama-c.html
are accurate ONLY FOR OLDER VERSIONS of opam.
For reference, these OUTDATED instructions are (do NOT use them):
# 1. Install opam (OCaml package manager)
sudo apt install opam # or dnf, pacman, etc.
# 2. Install Frama-C's dependencies
opam install depext
opam depext frama-c
# 3. Install Frama-C itself
opam install frama-cAfter installation, you may experience bash: frama-c: command not found
Try:
$ opam switch list
# switch compiler description
-> default ocaml.4.13.1 default
[WARNING] The environment is not in sync with the current switch.
You should run: eval $(opam env)So we run eval $(opam env) as directed
and now frama-c command works as expected.
If you find that you have to run eval $(opam env)
for every new terminal that you open and this is annoying,
then add eval $(opam env) to your ~/.bashrc.
If the summary was not informative enough, the rest of the document goes step by step and includes printouts and some troubleshooting.
$ pamac install opam
Preparing...
Synchronizing package databases...
Choose optional dependencies for opam:
1: darcs: For downloading packages with darcs
Enter a selection (default=none):
Warning: manjaro-hello: local (0.6.7-2) is newer than extra (0.6.6-11)
Warning: python-pyqt5: local (5.15.6-7.1) is newer than extra (5.15.6-7)
Resolving dependencies...
Checking inter-conflicts...
To install (3):
ocaml 4.13.1-1 (Required By: opam) extra
ocaml-compiler-libs 4.13.1-1 (Required By: opam) extra
opam 2.1.2-1 community
Total installed size: 437.4 MB
Apply transaction ? [y/N] y
Checking keyring... [3/3]
Checking integrity... [3/3]
Loading packages files... [3/3]
Checking file conflicts... [3/3]
Checking available disk space... [3/3]
Installing ocaml (4.13.1-1)... [1/3]
Installing ocaml-compiler-libs (4.13.1-1)... [2/3]
Installing opam (2.1.2-1)... [3/3]
Running post-transaction hooks...
Arming ConditionNeedsUpdate... [1/1]
Transaction successfully finished.$ opam --version
2.1.2
$ ocaml --version
The OCaml toplevel, version 4.13.1We visit https://www.frama-c.com/html/get-frama-c.html and look at the installation instructions for Linux.
The first step is:
# 1. Install opam (OCaml package manager)
sudo apt install opam # or dnf, pacman, etc.We already installed opam.
The second step is:
# 2. Install Frama-C's dependencies
opam install depext
opam depext frama-cLet's try that:
$ opam install depext
[ERROR] Opam has not been initialised, please run `opam init'Okay, let's run opam init:
$ opam init
No configuration file found, using built-in defaults.
Checking for available remotes: rsync and local, git, mercurial.
- you won't be able to use darcs repositories unless you install the darcs
command on your system.
<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised
<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><><><>
In normal operation, opam only alters files within ~/.opam.
However, to best integrate with your system, some environment variables
should be set. If you allow it to, this initialisation step will update
your bash configuration by adding the following line to ~/.bash_profile:
test -r /home/myuser/.opam/opam-init/init.sh && . /home/myuser/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true
Otherwise, every time you want to access your opam installation, you will
need to run:
eval $(opam env)
You can always re-run this setup with 'opam init' later.
Do you want opam to modify ~/.bash_profile? [N/y/f]
(default is 'no', use 'f' to choose a different file) y
User configuration:
Updating ~/.bash_profile.
[NOTE] Make sure that ~/.bash_profile is well sourced in your ~/.bashrc.
<><> Creating initial switch 'default' (invariant ["ocaml" {>= "4.05.0"}] - initially with ocaml-system)
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml" {>= "4.05.0"}]
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed base-bigarray.base
-> installed base-threads.base
-> installed base-unix.base
-> installed ocaml-system.4.13.1
-> installed ocaml-config.2
-> installed ocaml.4.13.1
Done.
# Run eval $(opam env --switch=default) to update the current shell environment$ eval $(opam env --switch=default)
$Let's try step 2 again:
$ opam install depext
[ERROR] depext unmet availability conditions, e.g. 'opam-version >=
"2.0.0~beta5" & opam-version < "2.1"'If we look at https://opam.ocaml.org/packages/depext/ we see:
This package has been renamed to 'opam-depext' and can safely be removed
So let's try installing that instead:
$ opam install opam-depext
The following actions will be performed:
- install opam-depext 1.2.1
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved opam-depext.1.2.1 (https://opam.ocaml.org/cache)
-> installed opam-depext.1.2.1
Done.
<><> opam-depext.1.2.1 installed successfully <><><><><><><><><><><><><><><><><>
=> opam-depext is unnecessary when used with opam >= 2.1. Please use opam
install directly insteadNow for the second part of step 2:
$ opam depext frama-c
You are using opam 2.1+, where external dependency handling has been integrated: consider calling opam directly, the 'depext' plugin interface is provided for backwards compatibility only
# Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=manjaro, os-family=arch
# The following system packages are needed:
cairo
which
zlib
Allow installing depexts via opam ? [Y/n] nOkay, we've been told twice that depext is unnecessary.
Let's skip forward to step 3 of Get Frama-C:
$ opam install frama-c
The following actions will be performed:
- install seq base [required by alt-ergo-lib]
- install conf-pkg-config 2 [required by conf-gtksourceview3]
- install cmdliner 1.0.4 [required by alt-ergo]
- install conf-gmp 4 [required by zarith]
- install dune 2.9.3 [required by ocamlgraph, lablgtk3,
alt-ergo, etc.]
- install conf-which 1 [required by conf-autoconf]
- install ocamlfind 1.9.3 [required by frama-c]
- install conf-zlib 1 [required by camlzip]
- install conf-gtksourceview3 0+2 [required by frama-c]
- install conf-gtk3 18 [required by lablgtk3]
- install conf-cairo 1 [required by cairo2]
- install stdlib-shims 0.3.0 [required by ocamlgraph]
- install result 1.5 [required by dune-configurator]
- install menhirSdk 20211128 [required by menhir]
- install menhirLib 20211128 [required by menhir]
- install easy-format 1.3.2 [required by yojson]
- install csexp 1.5.1 [required by dune-configurator]
- install cppo 1.6.8 [required by yojson]
- install conf-graphviz 0.1
- install conf-autoconf 0.1 [required by frama-c]
- install zarith 1.12 [required by frama-c]
- install num 1.4 [required by why3]
- install camlzip 1.11 [required by why3]
- install ocamlgraph 2.0.0 [required by frama-c]
- install menhir 20211128 [required by alt-ergo, why3]
- install biniou 1.2.1 [required by yojson]
- install dune-configurator 2.9.3 [required by alt-ergo-lib, cairo2]
- install ocplib-simplex 0.4 [required by alt-ergo-lib]
- install why3 1.4.1 [required by frama-c]
- install psmt2-frontend 0.4.0 [required by alt-ergo-parsers]
- install yojson 1.7.0 [required by frama-c]
- install cairo2 0.6.2 [required by lablgtk3]
- install alt-ergo-lib 2.4.1 [required by alt-ergo]
- install lablgtk3 3.1.2 [required by frama-c]
- install alt-ergo-parsers 2.4.1 [required by alt-ergo]
- install lablgtk3-sourceview3 3.1.2 [required by frama-c]
- install alt-ergo 2.4.1 [required by frama-c]
- install frama-c 24.0
The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated
-wp-prover native:alt-ergo)
===== 38 to install =====
Do you want to continue? [Y/n] Y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved alt-ergo.2.4.1 (https://opam.ocaml.org/cache)
-> retrieved biniou.1.2.1 (https://opam.ocaml.org/cache)
-> retrieved alt-ergo-lib.2.4.1 (https://opam.ocaml.org/cache)
-> retrieved cairo2.0.6.2 (https://opam.ocaml.org/cache)
-> retrieved camlzip.1.11 (https://opam.ocaml.org/cache)
-> retrieved cmdliner.1.0.4 (https://opam.ocaml.org/cache)
-> installed conf-pkg-config.2
-> installed conf-which.1
-> installed conf-gmp.4
-> installed conf-gtk3.18
-> installed conf-cairo.1
-> installed conf-gtksourceview3.0+2
-> installed conf-zlib.1
-> installed conf-autoconf.0.1
-> installed conf-graphviz.0.1
-> retrieved cppo.1.6.8 (https://opam.ocaml.org/cache)
-> retrieved csexp.1.5.1 (https://opam.ocaml.org/cache)
-> retrieved alt-ergo-parsers.2.4.1 (https://opam.ocaml.org/cache)
-> retrieved easy-format.1.3.2 (https://opam.ocaml.org/cache)
-> retrieved dune.2.9.3 (https://opam.ocaml.org/cache)
-> installed cmdliner.1.0.4
-> retrieved frama-c.24.0 (https://opam.ocaml.org/cache)
-> retrieved lablgtk3.3.1.2 (https://opam.ocaml.org/cache)
-> retrieved menhir.20211128 (https://opam.ocaml.org/cache)
-> retrieved menhirLib.20211128 (cached)
-> retrieved menhirSdk.20211128 (cached)
-> retrieved num.1.4 (https://opam.ocaml.org/cache)
-> retrieved ocamlfind.1.9.3 (https://opam.ocaml.org/cache)
-> retrieved lablgtk3-sourceview3.3.1.2 (https://opam.ocaml.org/cache)
-> retrieved ocplib-simplex.0.4 (https://opam.ocaml.org/cache)
-> retrieved ocamlgraph.2.0.0 (https://opam.ocaml.org/cache)
-> retrieved dune-configurator.2.9.3 (https://opam.ocaml.org/cache)
-> installed seq.base
-> retrieved psmt2-frontend.0.4.0 (https://opam.ocaml.org/cache)
-> retrieved result.1.5 (https://opam.ocaml.org/cache)
-> retrieved stdlib-shims.0.3.0 (https://opam.ocaml.org/cache)
-> retrieved yojson.1.7.0 (https://opam.ocaml.org/cache)
-> retrieved zarith.1.12 (https://opam.ocaml.org/cache)
-> installed ocamlfind.1.9.3
-> installed camlzip.1.11
-> retrieved why3.1.4.1 (https://opam.ocaml.org/cache)
-> installed num.1.4
-> installed zarith.1.12
-> installed ocplib-simplex.0.4
-> installed dune.2.9.3
-> installed stdlib-shims.0.3.0
-> installed csexp.1.5.1
-> installed easy-format.1.3.2
-> installed result.1.5
-> installed menhirSdk.20211128
-> installed menhirLib.20211128
-> installed cppo.1.6.8
-> installed biniou.1.2.1
-> installed dune-configurator.2.9.3
-> installed ocamlgraph.2.0.0
-> installed yojson.1.7.0
-> installed cairo2.0.6.2
-> installed alt-ergo-lib.2.4.1
-> installed lablgtk3.3.1.2
-> installed menhir.20211128
-> installed lablgtk3-sourceview3.3.1.2
-> installed psmt2-frontend.0.4.0
-> installed alt-ergo-parsers.2.4.1
-> installed alt-ergo.2.4.1
-> installed why3.1.4.1
-> installed frama-c.24.0
Done.
<><> frama-c.24.0 installed successfully ><><><><><><><><><><><><><><><><><><><>
=> Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect
# Run eval $(opam env) to update the current shell environmentNOTICE CAREFULLY that we have been given 3 commands to run:
$ rm -f ~/.why3.conf
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/myuser/.why3.conf
$ eval $(opam env)
$We will be using
https://github.com/AllanBlanchard/tutoriel_wp/blob/f4c1be54e6b2a315836cc125ce7f0ed5f24b2afc/code/program-proof-and-our-tool/frama-c/verify.c
to verify that our install/setup is correct.
$ cat verify.c
/*@
requires \valid(a) && \valid(b);
assigns *a, *b;
ensures *a == \old(*b);
ensures *b == \old(*a);
*/
void swap(int* a, int* b){
int tmp = *a;
*a = *b;
*b = tmp;
}
int main(){
int a = 42;
int b = 37;
swap(&a, &b);
//@ assert a == 37 && b == 42;
return 0;
}$ frama-c -wp -rte verify.c
[kernel] Parsing verify.c (with preprocessing)
[rte] annotating function main
[rte] annotating function swap
[wp] 10 goals scheduled
[wp] Proved goals: 10 / 10
Qed: 7 (0.30ms-1ms-3ms)
Alt-Ergo 2.4.1: 3 (6ms-7ms) (40)
[wp:pedantic-assigns] verify.c:13: Warning:
No 'assigns' specification for function 'main'.
Callers assumptions might be imprecise.$ frama-c-gui -wp -rte verify.c causes the GUI to launch successfully,
Inconsistently, I see the following printed in the terminal
when running the frama-c-gui command above,
but the GUI program seems to be fine.
(frama-c-gui:101764): GLib-CRITICAL **: 15:37:56.065: Source ID 7 was not found when attempting to remove it
To be redundant and clear, the versions used are:
$ opam --version
2.1.2
$ ocaml --version
The OCaml toplevel, version 4.13.1
$ frama-c --version
24.0 (Chromium)
$ frama-c-gui --version
24.0 (Chromium)Success! Frama-C is installed and working.
Side-note: From where did we find verify.c?
It is mentioned in this PDF:
https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
which is linked from:
https://www.frama-c.com/fc-plugins/wp.html