How launch the installed frama-c?

[TaihuLight]

I have installed frama-c and its gui by running: opam init opam install depext opam depext frama-c opam install frama-c

$ opam show frama-c package: frama-c version: 20171101 $ opam list frama-c Available packages for system: frama-c 20171101 Platform dedicated to the analysis of source code written

But I run it, it tips errors as follow: $ frama-c The program 'frama-c' is currently not installed. You can install it by typing: sudo apt install frama-c-base $ frama-c-gui The program 'frama-c-gui' is currently not installed. You can install it by typing: sudo apt install frama-c

how can i launch the frama-c-gui?

[tantignac]

The reason why it does not work might be Opam has not been propery set up. Please have a look at this comment on a similar StackOverflow thread: https://stackoverflow.com/questions/44323534/installing-frama-c-on-ubuntu#comment75653926_44323597

[maroneze]

The error messages of the sort The program 'frama-c' is currently not installed. ... are Debian-related and would suggest installing the apt packages, which we currently do not recommend. They appear because frama-c was not found in the PATH, and that is possibly because the shell environment did not get the proper values from OPAM.

As mentioned by @tantignac, the issue is likely that after installing OPAM, it was not enabled in your current shell (via eval $(opam config env) or something equivalent). Note that the opam binary itself is in your PATH (since opam- related commands are working), but not necessarily the environment that it sets up. If doing eval $(opam config env) is not enough to make it work, then there might be another issue. For instance, the fact that OPAM said:

Available packages for system:

Means that it is using a system-installed OCaml compiler, and not the version it compiled itself. That version does seem compatible with Frama-C (since the package is marked as available), but it is not always the best idea to have a mixed configuration (OCaml compiler installed via the OS, but other packages installed via OPAM), since it has already led to some issues in the past. Setting up a different ocaml switch might be useful. Then again, it is possible that you have already installed a OCaml switch via OPAM, but due to the lack of eval $(opam config env), it might have picked up an existing OCaml compiler from the OS. Hopefully OPAM 2.0 will avoid such issues in the future.

[TaihuLight]

Ubuntu 16.04.3在线安装Frama-C & Why/Coq From: http://www.cas.mcmaster.ca/~kahl/CS3EA3/2014/FramaC-installation.html On Ubuntu, before using Opam to install Frama-C etc.: (and probably similarly on many other binary Linux distributions): For essential software development tools, you need: sudo apt-get install build-essential m4 autoconf libgmp-dev libgnomecanvas2-dev libgtk2.0-dev libgtksourceview2.0-dev (See e.g. here for more info.) Although many dynamically-linked libraries are already installed on your systems, binary Linux distributions normally don't install the associated header files. Those header files typically reside in packages with names ending in -dev. When OPAM fails to install OPAM package conf-XYZ, then you will likely need package XYZ-dev (or at least XYZ) from your Linux distribution. 1) 执行$ sudo apt install opam命令在线安装opcam工具包 2) 将opam的路径添加到PATH环境变量中，即执行$ gedit ~/.bashrc打开文件后，新增如下命令 export PATH=/usr/bin/opam:$PATH This takes effect the next time you log out and back in. Until then, it also tells you what command to run to set up your environment without logging out. 执行$ source ~/.bashrc使设置的环境变量生效，执行$opam，若输出opam信息则表示opam安装并设置成功，否则需要重新安装或设置环境变量。 3) 执行如下命令采用opam在线安装frama-c及其插件why $ opam init $ opam install depext $ opam depext frama-c $ opam install frama-c why altgr-ergo 4) 执行$ frama-c-gui命令, 若安装成功将会启动图形化Frama-C工具。 5) 插件coq安装过程参见https://github.com/coq/coq 6) Demo for code split(程序切片) https://stackoverflow.com/questions/46437037/how-to-install-impact-analysis-plug-in-for-frama-c-on-ubuntu-14-04 https://stackoverflow.com/questions/47208799/slicing-a-c-code-with-frama-c

[mehdid]

Should we remove frama-c packages from Debian? (if it is not recommended)

[maroneze]

Sorry, I misstated the intent of the recommendation: we do not recommend mixing opam and distribution packages, because that tends to confuse findlib and weird errors have been reported related to it. Since the user had reported using opam already, I wanted them to avoid installing the Debian package at the same time.

Some clarifications have been added to that effect to INSTALL.md, and should be available in the next release.

[maroneze]

Given the fixes and changes in the latest release, I'm closing this issue. Feel free to reopen in case you still have problems with it.