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] Why wp plugin failed to prove such naive properties?

  • Subject: [Frama-c-discuss] Why wp plugin failed to prove such naive properties?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Sun, 10 Nov 2013 19:57:44 +0000
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>