--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on November 2013 ---
Another issue is "How does frama-c prove the assigns clause?" In my point of view, the assign means that the locs is assigned in this function. But the following property (labeled with "C") was also proved to be valid in frama-c(I am using the wp plugin to prove the contract). But the "Arr" parameter was only used but not to be defined in the function test. The "NoUse" parameter never used in this function at all. Am I wrongly understand the assign clause? Thanks. /*@ requires \valid(Arr); ensures A: Arr == \old(Arr); ensures B: *\old(Arr) == \old(*Arr); assigns C: *Arr, *NoUse; */ int test(int *Arr, int index, int *NoUse) { return Arr[index]; } On 10 November 2013 19:57, David Yang <abiao.yang at gmail.com> wrote: > > 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/a24dda52/attachment.html>