--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why wp plugin failed to prove such naive properties?



Dear all,

I am new to formal verification. I just want to learn something about it.

I used the wp plugin to prove some properties for function min in test.c
file. (see in below)

Why I can't prove the property B and C? I only get the minimal value of the
array A.

But it seems that the property B and C are obviously correct.

Why it failed to prove these properties?

Thank you very much for any suggestions.

Regards,
David


the command I used for :
$ frama-c text.c -wp -wp-fct min

the result is :
...
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_exam_post_A : Valid
[wp] [Alt-Ergo] Goal typed_exam_post_C : Unknown (1s)
[wp] [Alt-Ergo] Goal typed_exam_post_B : Unknown (1s)


// test.c
/*@
requires \valid(Arr) && \valid(Arr+(0..size-1));
 ensures A: Arr == \old(Arr);
ensures B: *\old(Arr) == \old(*Arr);
ensures C: \forall integer i; 0 <= i <= size - 1 ==> Arr[i] == \old(Arr[i]);
  */
int min(int *Arr, int size)
{
int index = 0;

int min = Arr[0];

while(index <= size - 1){
if(min > Arr[index])
min = Arr[index];

index = index + 1;
}
return min;
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131110/1adfdea9/attachment.html>