--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on November 2013 ---
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>