--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis and approximaitons



Hello Frama-C!

    I am a new user and I am most interested in Value Analysis. I have written a very small program which intends to build for a variable (here it is called "s") a set of values. In the program, the values come from the array called "v", through some indirections.

    Running my small program with -val will give the following results s ? {1; 2; 3; 4; 5; 107; 110; }, which is "as expected". However, as soon as I change the interval to (0,7), I get s ? [1..110], which is obviously an approximation. 

    Question is: how can I stop frama-c from making this approximation and instead to feed me the result of s ? {1; 2; 3; 4; 5; 107; 108; 110;  }?

    Thank you very much for your time!

#include "builtin.h"
typedef struct s
{
 int n;
 int *p;
} S;


int v[10]={1,2,3,4,5,110,107,108,109,106};

S big={10,v};
void main(void)
{
 int i;
 int s=0;
 s=big.p[Frama_C_interval(0,6)];
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100517/2fdac3c8/attachment.htm>