3

I installed Frama-c on Ubuntu 14.04, using the following commands:

sudo apt-get install frama-c

However, when I open the GUI of frama-c using the following command:

frama-c-gui

I cannot find the "Impact Analysis" plug-in on the left-hand side window.

This figure shows currently available plug-in of my Frama-c: Figure 1

I also referred to the Frama-c web page but cannot find any links for me to download or install the Impact Analysis plug-in.

How can I enable and use the Impact Analysis on Ubuntu 14.04?

Gilles 'SO- stop being evil'
  • 104,111
  • 38
  • 209
  • 254
shashibici
  • 33
  • 3
  • As you can see in my edited message, the unfortunate answer is that, with such an old version of Frama-C (distributed in Ubuntu 14.04), you cannot use the Impact plug-in, you have to upgrade to a more recent Frama-C version. – anol Sep 28 '17 at 17:02
  • Thanks! I have used OPAM, and now everything is going correctly. – shashibici Sep 29 '17 at 17:07

1 Answers1

2

The Impact plug-in is already installed with Frama-C since version Neon-20140301, and you do not need to do anything special to enable it, just select a statement and find the right context menu to activate it.

From the Frama-C web page that you mentioned (highlighting in bold the relevant part):

Impact analysis is available through a contextual menu at each statement in the Frama-C graphical user interface.

The left-hand side window in your screenshot contains the filetree (upper part, with file names and global variables/functions), and a list of plug-in panels, for those plug-ins which registered their own GUI panels. Note that not all plug-ins have associated panels; Impact, for instance, is a plug-in that is made available only via contextual menus.

Looking closely at the Impact plug-in page in the Frama-C website, you'll notice that the screenshot shown does not include the part of the GUI in your screenshot, but instead, its left part is already the Cil code (omitted in your screenshot):

Frama-C Impact plug-in GUI

To obtain the popup menu indicated in the screenshot, you need to have a statement highlighted, not just an expression. Note that, in the screenshot, the entire p = T; statement is highlighted. Otherwise, the context menu will not show the "Impact analysis" item.

An easy way to select a statement in the Frama-C GUI is to click after the semicolon. If it's an assignment statement, as in the screenshot above, you can also click on the equals sign to select the statement. However, if you click on p or T directly, you will select only the expression corresponding to those variables. Because Impact is based on statements, not expressions, it will not show its context menu in such cases.

By the way, if you want to check if a given plug-in is available in your Frama-C installation, you can simply run frama-c -plugins to obtain the list of installed plug-ins, or open the Analyses panel in the GUI (menu Analyses/Analyses), which contains one entry per plug-in.

Edit: after testing with a VM, I realized that Ubuntu 14.04 (Trusty) has Frama-C Fluorine (from 2013) in its packages, which is a very old version that did have the Impact plug-in, but for some reason it was not included in the Debian package at the time (which is why you cannot use it). Frama-C is rapidly evolving, so using such an old version will result in several issues. I really recommend trying to install it via OPAM.

anol
  • 8,264
  • 3
  • 34
  • 78
  • I did the exact what you said (clicking on the statement instead of an expression) but I still cannot see the "Impact analysis" option. In addition, I run `frama-c -plugins` but it ends up telling me that option `-plugins` is unknown. I am wondering whether Frama-c has been installed correctly, by just using `apt-get install frama-c`. – shashibici Sep 28 '17 at 15:51
  • You are probably using Frama-C Sodium or older, in which case `frama-c -help` should list the available plug-ins. Can you please run `frama-c -version` and tell which version you are using? – anol Sep 28 '17 at 16:02
  • By the way, using the Frama-C Debian/Ubuntu packages is no longer the preferred way to install Frama-C (in particular, it will install an old release); the [recommended way](http://frama-c.com/install-phosphorus-20170501.html) is via OPAM, the OCaml Package Manager. It does however require more effort than using apt-get. The advantage is that you will be able to upgrade to newer releases of Frama-C. – anol Sep 28 '17 at 16:12