[Frama-c-discuss] a value analysis case studie
stephane.duprat at atosorigin.com
Sun Oct 17 23:52:32 CEST 2010
Here is a small test where I can't find the good manner to succed in
value analysis :(
Here is a f1 function,
//@ requires 0<=n<5;
int f1(int n)
res = init1();
if (res == 0)
This is a simplified example of real case where the program is always
strucutured by an init procedure followed by the functional body.
The init procedure could be complex and could fail in some cases.
That's why a status is returned by the init procedure and the functional
part is applied only if the init succeds.
As a consequence, the functional part should take as environment values
of the program is case of success only. That is my problem with the
I've tried a simplified case of this situation wich illustrates the same
In this trivial case, the functional part is just the statement "return
tab[index+n];" and it needs that index is 0, that is true due to the
init1() procedure in case of success. And the init procedure is init1().
But values computed by the tool for index at the exit of init1() is
[--...--]. And there is no relational properties between the exit status
of init1() and index (for ex: "\result ==0 => index==0").
And I catch this false alarm :
file1.c:30:[kernel] warning: accessing out of bounds index. assert
((0 ≤ (int )(index+n)) ∧
((int )(index+n) < 5));
I'm wondering if value analysis experts have a solution to avoid this
false alarm ?
source example in attached file.
thanks in advance,
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the Frama-c-discuss