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] a value analysis case studie

  • Subject: [Frama-c-discuss] a value analysis case studie
  • From: stephane.duprat at atosorigin.com (Stephane Duprat)
  • Date: Sun, 17 Oct 2010 23:52:32 +0200
  Hello,

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 
difficulties.
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,


St?phane



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