Make Frama-c show dependencies even of "dead branches"

Question

I am using frama-c Aluminium-20160502 version and I want to find out the dependencies in a large program. When using the option -deps in the command line I found some dependencies are missing. In particular when several conditions are joined in one if, the dependency analysis stops whenever one condition is false. In this example here:

#include<stdio.h>
#include<stdbool.h>

/*Global variable definitions*/
bool A = true;
bool B = false;
bool C = true;
bool X;
bool Y;

bool res;


void main(){

        if (A && B && C) {
                res = X;
        }else res = Y;
}

when I try: frama-c -deps program.c

frama shows the following dependencies:

[from] ====== DEPENDENCIES COMPUTED ======

These dependencies hold at termination for the executions that terminate:

[from] Function main: res FROM A; B; Y

[from] ====== END OF DEPENDENCIES ======

so it does not reach the condition C because already B is false.

I wonder if there is a way to tell frama to compute all dependencies even if the condition is not fulfilled. I tried with the option -slevel but with no results. I know there is a way to use an interval Frama_C_interval(0,1) but when I use it the variable using this function is not shown in the dependencies. I would like to get X and Y dependent on A,B,C and res dependent on A,B,C,X,Y

Any ideas?

Answer 1

The From plugin uses the results of the Value analysis plugin. In your example, the values of A and B are sufficiently precise that Value is able to infer that the condition is entirely determined (since the && operator is lazily evaluated, from left to right) before reaching C, therefore C never affects the outcome and is thus not a dependency from the point of view of From.

Unfortunately, Frama_C_interval cannot be used directly at global initializers:

user error: Call to Frama_C_interval in constant.

You can, however, use a "hack" (not always the best solution, but works here):

volatile bool nondet;
bool A = nondet;
bool B = nondet;
bool C = nondet;
...

Note that because nondet is volatile, each variable A, B and C is assigned a different non-deterministic value.

In this case, Value has to consider both branches of the conditionals, and therefore C becomes a dependency in your example, since it is possible that C will be read during the execution of main. You'll then have:

       These dependencies hold at termination for the executions that terminate:
[from] Function main:
  res FROM A; B; C; X; Y

Note that some plugins require special treatment when dealing with volatile variables, so this is not always the best solution.

This however only deals with some kinds of dependencies. As mentioned in Chapter 6 of the Value Analysis user manual, the From plugin computes functional, imperative and operational dependencies. These do not include indirect control dependencies, which are those such as X from A, B, C, as you mention. For those, you need the PDG (Program Dependence Graph) plugin, but it does not currently have a textual output of the dependencies. You can use -pdg to compute it, and then -pdg-dot <file> to export the dependency graph in dot (graphviz) format. Here's what I get for your main function (using the volatile hack as mentioned previously):

Finally, as a side note: -slevel is mostly used to improve precision, but in your example you already have too much precision (that is, Value is already able to infer that C is never read inside main).