--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] About the memory separation and the usage of '\separated'



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>