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] About the memory separation and the usage of '\separated'

  • Subject: [Frama-c-discuss] About the memory separation and the usage of '\separated'
  • From: wuwenhao at udel.edu (Wenhao Wu)
  • Date: Fri, 3 Mar 2017 15:59:51 -0500
Hi all,

I am Wenhao Wu, a grad-student of the University of Delaware.
Currently, I encounter a problem related with the notion '\separated'.

I am trying to verify a function that copies the data from a given input
array
with a given length into a local pointer and then returns the pointer.

Here is the command of using frama-c

frama-c -wp -wp-model Typed+var+nat+real -wp-prover why3ide arr_copy.c

Here is the whole program:

/*@ requires 0 < len;
>   @ ensures \valid(\result+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> \result[j] == 0);
>  */
> int* arr_init(int len); //{ return (int*)calloc(len, sizeof(int)); }
>
> /*@ requires 0 < len;
>   @ requires \valid(in_arr+(0 .. len-1));
>   @ ensures \valid(\result+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> \result[j] == in_arr[j]);
>  */
> int* arr_copy1(int len, int* in_arr){
>     int i = 0;
>     int * out_arr = arr_init(len);
>     //@ assert \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1));
>
>     /*@ loop invariant 0 <= i <= len;
>       @ loop invariant \forall integer j;
>       @      ((0 <= j < i) ==> out_arr[j] == in_arr[j]);
>       @ loop assigns out_arr[0 .. len-1], i;
>       @ loop variant (len-i);
>      */
>     while(i < len){
>         out_arr[i] = in_arr[i];
>         i = i + 1;
>     }
>     return out_arr;
> }


The verification of the *loop invariant* (marked by blue color) depends on
that the *assertion* (marked by red color).

If the local pointer 'out_arr' is assigned by the result returned by
the function 'init(int len)', which uses calloc(size_t num, size_t type)
function,
then the assertion is expected to be true.

Thus, I wonder whether there is a way to assume a condition of
' \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1)) ' to be true,
or to specify a pre-condition like
' \separated(in_arr+(0 .. len-1), \result+(0 .. len-1)) '.

May I ask for some suggestions that help me to
verify the function " *int*** arr_copy1(**int len, int*** in_arr)* "?
Or is there any way to assume/define the memory space
allocated (by malloc or calloc) is separated from other
used memory space?

And another version of the function copying an array is proved.
The function and its contract is shown here:

/*@ requires 0 < len;
>   @ requires \valid(in_arr+(0 .. len-1)) &&
>   @          \valid(out_arr+(0 .. len-1));
>   @ requires \separated(in_arr+(0 .. len-1), out_arr+(0 .. len-1));
>   @ ensures \valid(out_arr+(0 .. len-1));
>   @ ensures \forall integer j;
>   @   (0 <= j < len ==> in_arr[j] == out_arr[j]);
>   @ assigns out_arr[0 .. len-1];
>  */
> void array_copy2(int len, int * in_arr, int * out_arr){
>     int i = 0;
>
>     /*@ loop invariant 0 <= i <= len;
>       @ loop invariant \forall integer j;
>       @      ((0 <= j < i) ==> out_arr[j] == in_arr[j]);
>       @ loop assigns out_arr[0 .. len-1], i;
>       @ loop variant (len-i);
>      */
>     while(i < len){
>         out_arr[i] = in_arr[i];
>         i = i + 1;
>     }
> }


All scheduled goals can be proved by Alt-Ergo (1.30)

Sincerely,
Wenhao Wu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170303/b64f9a6b/attachment.html>