Explicit-value analysis in Frama C

Question

I am trying value analysis plugin of Frama-C as an abstract interpretation back-end in my project. In particular, this project is about translating a concurrent C program with POSIX thread to an equivalent sequential C program that simulates the corresponding concurrent program and using sequential analysis tools to analyze the sequential program (Cseq).

The plugin does provide very good approximation of values for variables in my programs. However, in order to make the back-end work, it is required that a specific set of variables in the sequential program are tracked precisely, for which it is called explicit-value analysis (influence from this paper explicit-value-analysis). For example, for the variables representing the control-flow or the context switch points, their values need to be precisely tracked at each statement (a specific value), not just in an enumeration or an interval. I wonder if Frama-C provides this feature. If it is the case, I would deeply appreciate if someone can help me with this.

Pascal Cuoq Pascal Cuoq · Accepted Answer · 2015-02-08T13:19:26

This does not exist out of the box in Frama-C.

First, the discussion below assumes that you have already experimented with Frama-C's -slevel option and that you are using it.

If you are willing to add a statement each time an important variable is modified, you could change the program to something like this:

…
/* original assignment: */
important = important /* already known precisely */ + unimportant;
/* instrumentation: */
tis_variable_split(&important, sizeof important, LIMIT);
…

The builtin tis_variable_split takes the values that have just been computed for variable important and propagates as many abstract states as necessary, assigning important a single value in each of them.

The builtin tis_variable_split does not have an implementation in Frama-C (that I know of) but is available in TIS Analyzer, a commercially available static analyzer based on Frama-C. You can contact TrustInSoft, the company that sell it, about obtaining a license. Disclaimer: I work there.

If you know in advance the set of values that important can take, you can simulate the same effect with a disjunction:

/*@ assert important == value1 || important == value2 || … ; */

The assertion can grow unwieldy quite quickly, but since we are talking about an automatic instrumentation, it would only need to be small enough to be automatically generated and handled by the framework. It would be possible to modify the framework so that even the instrumentation step above is unnecessary. This modification would be work, so you would have to be prepared to explain in more detail the needs of your experiment so that whoever might do this work would not waste their time, and you would have to be prepared to share the scientific credit for the end result, which would then be the product of a collaboration.

Explicit-value analysis in Frama C

1 Answers