--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on October 2010 ---
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>