--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Example to understand -slevel influence on Value analysis's result



Hello,

I tried to explain how -slevel works at some colleague. I used the 
attached example.

I hope it will help others to get a clearer view on the behaviour of 
-slevel.

Best regards,
david
-------------- next part --------------
/* Test this program with:
    frama-c -val -slevel 1 slevel-example.c
and
    frama-c -val -slevel 2 slevel-example.c

And look at the value of "x".

With -slevel 1 we have "x ??? {2; 3; 4}" and with -slevel 2 with have "x
??? {2; 4}".

Why?

Because -slevel increases the number of different considered path for
the analysis.

In our program:

 -slevel   |    c       |     a      | g(c,a)                  |   x
------------------------------------------------------------------------------
  1        | c ??? {0; 1} | a ??? {2; 3} | g(c,a) ??? {(0,2); (1,2); | x ??? {2; 3; 4}
           |            |            |           (0;3); (1,3)} |
------------------------------------------------------------------------------
  2        |            |            |                         |
  |-path 1 | c ??? {0}    | a ??? {2}    | g(c,a) ??? {(0,2)}        | x ??? {2}
  \-path 2 | c ??? {1}    | a ??? {3}    | g(c,a) ??? {(1,3)}        | x ??? {4}
           |            |            |                         |
 aggregated| c ??? {0; 1} | a ??? {2; 3} |                         | x ??? {2; 4}
    result |

I hope result of Frama-C analysis is clearer now.

David Mentr??, 19th of June, 2014.

*/

extern int entropy_source;

/*@ assigns \result \from entropy_source;
    assigns entropy_source \from entropy_source;
    ensures \result == 0 || \result == 1; */
int f(void); // f() returns indeterministically 0 or 1

int g(int x, int y)
{
  return x + y;
}

void main(void)
{
  int c;
  int a = 2;
  int x;

  c = f();

  if (c) {
    a = 3;
  }

  x = g(c, a);
}