--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Specification Examples



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