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 23:51:54 +0000
  • In-reply-to: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com>
  • References: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com>
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>