Understanding Frama-C slicer results

frama-c, slice

Solution

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;
}

Problem

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

Original source