Search code examples
cubuntuframa-cprogram-slicing

How to install Impact Analysis Plug-in for Frama-c on Ubuntu 14.04?

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?

Solution

  • 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.