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] New Specification Examples

  • Subject: [Frama-c-discuss] New Specification Examples
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Tue Oct 14 14:14:53 2008
  • In-reply-to: <48F47FE2.4080308@inria.fr>
  • References: <41A1C9B7510644ABBFFD7ABB57065E88@AHARDPLACE> <48F47FE2.4080308@inria.fr>
Hello,
thank you for answering. After I sent the mail we discovered my error, the 
trivial ensures clause is just for the eye.

But updating my example I discovered something else.

/*@
 requires last >= first;
 requires \valid_range(first, 0, (last-first)/sizeof(int)-1);
 behavior is_not_empty:
  assumes last > first;
  ensures  \forall integer i; 0 <= i < (last-first)/sizeof(int) ==> first[i] 
== value;
 behavior is_empty:
  assumes last == first;
  ensures last == first;

*/
void fill_int_array (int* first, int* last,  int value );

I dont know how Frama-C handles the pointer substraction but i guess its 
done as in C, meaning i would get a big number and not the count of the 
fields in my array.
It seams as if the sizeof has not yet been implemented in the Hydrogen, i 
get the error:

Fatal error: exception Assert_failure("src/jessie/interp.ml", 354, 1)

Is it implemented in the Helium release or even later?

Will this be automated in the next release or will I allways have to use the 
division with sizeof() to get to the length of my array.

Christoph

----- Original Message ----- 
From: "Claude March?" <Claude.Marche@inria.fr>
To: <frama-c-discuss@lists.gforge.inria.fr>
Sent: Tuesday, October 14, 2008 1:17 PM
Subject: Re: [Frama-c-discuss] New Specification Examples



I have a hard time to follow each iteration in this example, but I would
like to emphasize a fundamental mistake here.

Christoph Weber wrote:
> /*@
>  requires last >= first;
>  requires \valid_range(first, 0, last-first-1);
>  behavior is_not_empty:  assumes last > first;
>   ensures  \forall integer i; 0 <= i < last-first ==> first [i] == value;
>  behavior is_empty:
>   assumes last == first;
>   ensures last == first; */
> void fill_int_array (int* first, int* last,  int value ) {
 > ...
 > }

> In this example the ensurance of the postcondition does not work due to 
> the changing value of first.

Wrong, from the caller point of view, parameters (like first and last)
do not change (there are not modifiable lvalues)

Consequently, any use of \old on them like in \old(first) is useless.
Also, the ensures clause last==first in behavior is_empty is a
triviality (from the assumes clause)

Hope this helps,

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |







_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss@lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss