--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on March 2017 ---
Hi Wenhao, Actually, the WP-plugin is not already implementing the ACSL annotations describing allocation. However, in the internal memory model of WP, addresses are partitioned into regions, described by an internal `region(integer) : integer` logic function. Regions 0,1,2 and <0 are reserved for WP for formals, locals, etc. You can use and region >= 3 for malloc. Hence, using an axiomatic, you can specify in regular ACSL the behaviour of allocation, by axiomatising a logical function returning pointers, such that the âk'-th returned pointer belongs to region 3+k (starting at 0). We can introduce the âkâ-th call to malloc with and the internal WP region with ACSL declarations and a ghost integer : //@ ghost int ALLOC = 3 ; logic integer WPREGION(int *addr) reads addr ; logic int* WPALLOC(integer k) reads k; To connect the WPREGION to the internal âregionâ function of WP we use a driver and an additional alt-ergo definition : $ cat alloc.driver library Malloc: memory altergo.file += "alloc.mlw" ; logic integer WPREGION( addr ) = "region_base » ; $ cat alloc.mlw function region_base ( a : addr ) : int = region( a.base ) To help specifying, we introduce the following ACSL predicates: // Necessary pre-condition for any allocating function. predicate Allocating{L} = 3 <= \at( ALLOC , L ) ; // The k-th allocated address since FROM. logic int *Alloc{FROM}(integer k) = WPALLOC(\at(ALLOC+k,FROM)); // Designate the k-th allocated address since FROM. predicate Allocated{FROM}(int *addr,integer k) = (WPREGION(addr) == \at(ALLOC+k,FROM)) && (addr == WPALLOC(\at(ALLOC+k,FROM))) ; // Number of allocated pointers between PRE and POST. predicate Allocates{PRE,POST}(integer n) = \at( ALLOC , POST ) == \at( ALLOC , PRE ) + n ; Typically, your allocating function `arr_init` shall be specified as follows: (modifications of your code in blue) /*@ requires 0 < len; @ requires Allocating ; @ ensures \valid(\result+(0 .. len-1)); @ ensures \forall integer j; @ (0 <= j < len ==> \result[j] == 0); @ ensures Allocates{Pre,Post}(1); @ ensures Allocated{Pre}(\result,1); @ assigns ALLOC ; */ int* arr_init(int len); //{ return (int*)calloc(len, sizeof(int)); } Then, the copy-function can be specified as follows: /*@ requires Allocating ; @ 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]); @ ensures Allocates{Pre,Post}(1); @ ensures Allocated{Pre}(\result,1); @ assigns Alloc{Pre}(1)[0..len-1]; @ assigns ALLOC ; */ int* arr_copy1(int len, int* in_arr){ ... } Then : $ frama-c -wp alloc.c -wp-driver alloc.driver [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing alloc.c (with preprocessing) [wp] warning: Missing RTE guards [wp] 22 goals scheduled [wp] Proved goals: 22 / 22 Qed: 15 (0.58ms-4ms-13ms) Alt-Ergo: 7 (14ms-58ms-243ms) (366) All files in attachment. Remark : in the experiment above, we keep your original separtion-assertion, which turned to be proved thanks to regions. However, such an assertion is no more necessary to prove the specifications, and you can remove it from your code. > Le 3 mars 2017 à 21:59, Wenhao Wu <wuwenhao at udel.edu> a écrit : > > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0004.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: alloc.mlw Type: application/octet-stream Size: 59 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0003.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0005.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: alloc.driver Type: application/octet-stream Size: 102 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0004.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0006.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: alloc.c Type: application/octet-stream Size: 1910 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0005.obj> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170306/02018745/attachment-0007.html>