Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] Example to understand -slevel influence on Value analysis's result
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Thu, 19 Jun 2014 10:43:00 +0200
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);
}