--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Problem with simple search programm



Hello Hollas,

I'm just another Frama-C user, so my reply is not authoritative.

On Wed, Mar 25, 2009 at 15:56, Hollas Boris (CR/AEY1)
<Boris.Hollas at de.bosch.com> wrote:
> Running Simplify results in two ? signs:
>
> - when I click on the first "?" labeled "postcondition", the following code is highlighted:
>
> insVal(int a[], int aLength, int val) {
> ?int i = 0;
>
> ?//@ loop in
>
> ?I don't understand what that means. Is this a bug in gWhy's highlighting?

I ran[1] your example on my own installation of Frama-C, the following
code is highlighted[2]:
"\result == true  <==>  \exists int j; 0 <= j <= aLength-1 && a[j] ="

which means the postcondition "ensures \result == true  <==>  \exists
int j; 0 <= j <= aLength-1 && a[j] == val;" is not verified.

So you might have an issue with your setup of Frama-C.

> - the second "?" is labeled "pointer dereferencing" and corresponds to
> ? ? ?if(a[i] == val) return true;
> ?Does this mean that frama-c doesn't detect that i<aLength holds at this point?

More exactly, the "if" is highlighted and in the upper right corner you see
"offset_min(int_P_a_20_alloc_table, a) <= integer_of_int32(i_27_0)"

It means that you must check that "i" does not access a[] outside of
a[] lower boundary.

You should add a loop invariant: "loop invariant i >= 0;"

With this added invariant, all properties are proven:
----
#define true 1
#define false 0
typedef int bool;


/*@
 requires \valid(a+ (0..aLength-1));
 ensures \result == true  <==>  \exists int j; 0 <= j <= aLength-1 &&
a[j] == val;
*/
bool ContainsVal(int a[], int aLength, int val) {
 int i = 0;

 /*@ loop invariant \forall int j; 0 <= j <= i-1 ==> a[j] != val;
     loop invariant i >= 0;
g  */
 while(i<aLength) {
     if(a[i] == val) return true;
     else i++;
 }
 return false;
}
------


Sincerely yours,
david



[1] Command line:
  frama-c -jessie-analysis -jessie-std-stubs -jessie-atp alt-ergo
-jessie-cpu-limit 2 -jessie-gui hollas-containsval.c

[2] This is a known bug:
https://gforge.inria.fr/tracker/index.php?func=detail&aid=7496&group_id=1123&atid=5488