Understanding Frama-C slicer results

Question

I'd like to know if it's possible to do some kind of forward conditioned slicing with Frama-C and I'm playing with some examples to understand how one could achieve this.

I've got this simple example which seems to result in an imprecise slice and I can't understand why. Here is the function I'd like to slice :

int f(int a){
int x;
if(a == 0)
    x = 0;
else if(a != 0)
    x = 1;
return x;
}

If I use this specification :

/*@ requires a == 0;
  @ ensures \old(a) == a;
  @ ensures \result == 0;
*/

then Frama-C returns the following slice (which is precise), using "f -slice-return" criterion and f as entry point :

/*@ ensures \result ≡ 0; */
int f(void){
  int x;
  x = 0;
  return x;
}

But when using this specification :

/*@ requires a != 0;
  @ ensures \old(a) == a;
  @ ensures \result == 1;
*/

then all instructions (& annotations) remain (when I was waiting for this slice to be returned :

/*@ ensures \result ≡ 1; */
int f(void){
  int x;
  x = 1;
 return x;
}

)

In the last case, is the slice imprecise? In this case, what could be the cause?

Regards,

Romain

Edit : I wrote "else if(a != 0) ..." but the problem remains with "else ..."

Answer 1

In Frama-C, the slicing plug-in relies on the result of a preliminary static analysis plug-in called the value analysis.

---

This value analysis can represent the values for variable a when a == 0 (the set of values is in this case { 0 }) but has a hard time to represent the values for a when it is known that a != 0. In the latter case, if a is not already known to be positive or negative, the value analysis plug-in needs to approximate the set of values for a. If a was known to be positive, for instance if it was an unsigned int, then the nonzero values could be represented as an interval, but the value analysis plug-in cannot represent “all values of type int except 0”.

---

If you are willing to change the pre-condition, you can write it in a form that is more easily understood by the value analysis plug-in (together with value analysis option -slevel):

$ cat t.c
/*@ requires a < 0 || a > 0 ;
  @ ensures \old(a) == a;
  @ ensures \result == 0;
*/

int f(int a){
int x;
if(a == 0)
    x = 0;
else if(a != 0)
    x = 1;
return x;
}
$ frama-c -slevel 10 t.c -main f -slice-return f -then-on 'Slicing export' -print 
…
/* Generated by Frama-C */
/*@ ensures \result ≡ 0; */
int f(void)
{
  int x;
  x = 1;
  return x;
}

Answer 2

This has no relevance whatsoever with your main question, but your ensures a == \old(a) clause is not doing what you expect. If you pretty-print your source code with option -print, you will see it has been silently transformed into ensures \old(a) == \old(a).

The ACSL language does not permit referring about the value of formal variables in the post-state, mostly because this is meaningless from the point of view of the caller. (The stack frame of the callee is popped after the call terminates.)