I had wasted almost half of a day trying to properly install frama-c on my Linux. I was surprised to see no much documentation or troubleshooting online, so that's the whole point of me putting this note as a public gist.
If you read the official documentation, you'll come across the names of these two packages:
frama-c and frama-c-base
If you are on Ubuntu 18.04 LTS, you can directly install it using apt install frama-c, and it will work. You can not do this on a 20.04 LTS Focal Fossa, because apparently, it's not included in the official packages.
All of the dependicies with the exact supported version (more on that later) is perfectly done on the packages for 18.04, but not for Focal Fossa.
Focal Fossa does have frama-c-base on their packages list, which I had tried installing, but it throwed an error related to one of the dependencies why3, which I couldn't solve even after installing it using aptitude.
Opam
Opam is the package manager for Ocaml, which I've heard, is a programming language made and used by llamas(cs joke).
You can get frama-c up and running using:
sudo apt install opam #gets opam
opam init #press y and allow it do configure your ~/.profile
eval $(opam env) # sets the environment variable on the current shell session
opam depext frama-c #gets frama-c's dependencies, I believe
opam install frama-c
This will take several minutes. It did, on my FreeBSD. This is also consumes large amount of disk space. You'd need GNU Make and Meson preinstalled, which you probably have already, as I think they come under GNU coreutils now.
Depending on your system, it may fail, telling you that it doesn't have one of its dependencies/packages. The only solution is to get that using your distribution's package manager. In my case, on my FreeBSD, using pkg and other ports. Some can be installed using opam install $lib_name, too. Try that.
You need the exact version of the dependencies to make it work. I had to downgrade gnomecanvas, which is one of the dependencies. The version it needs will be displayed on the error it displays after you run install. You can do something like opam install $package_name $version, to install the specefic version using opam. Try doing the equivalent on your distro's package manager, otherwise.
Run frama-c -v to see whether it has been installed properly: It'd return the frama-c version along with the code name of the version:
Try compiling a program too, to see if important packages like why3 have been configured correctly. Here's a sample program from the official website. You can check them all out over here
/*@ ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
int max (int x, int y) { return (x > y) ? x : y; }
root@freebsd:~/pr # frama-c -wp -wp-rte max.c
[kernel] Parsing max.c (with preprocessing)
[rte] annotating function max
[wp] 1 goal scheduled
[wp] [Cache] found:1
[wp] Proved goals: 1 / 1
Qed: 0 (8ms)
Alt-Ergo 2.2.0: 1 (16ms) (16) (cached: 1)
I had recieved this particular error when compiling a program:
[kernel] Parsing file.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
which was solved by running : why3 config --full-config
/thanks to yadhuz for this
All of the packages installed by opam is stored inside /home/$whoami/.opam/default/bin/, and thank god, it doesn't need the superuser privileges. That's the only thing I like about opam, this drastically reduces chances of screwing up an entire OS with this. That also means that, if you are done with opam and its super huge files, you can just remove stuff with ease. You can opam remove $package_name or just rm the files (not recomended), if that's not working.
I hope this helped.