[Frama-c-discuss] a value analysis case studie

Stephane Duprat 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)
int res;

res = init1();

if (res == 0)
return tab[index+n];

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 
value analysis.

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...
Name: file1.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101017/51c85f63/attachment.txt>

More information about the Frama-c-discuss mailing list