--- layout: fc_discuss_archives title: Message 129 from Frama-C-discuss on September 2013 ---
Hello, 2013/9/24 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>: > However, we would like to write a more precise assigns clause for the Interp > array that has two or three elements according to Itab value. > > In the requires and ensures clauses the Itab value was considered, for > example: > requires Itab != 1 ==> \valid_range (Interp,0,2); > > requires Itab == 1 ==> \valid_range (Interp,0,1); > > How to write the assigns clause for the Interp array taking in account the > Itab value? > The easiest way is to provide behaviors. Note in addition that \valid_range has been deprecated. You should use \valid instead: /*@ requires Itab == 0 || Itab == 1; behavior Itab_is_one: assumes Itab == 1; requires \valid(Interp + (0..1)); assigns Interp[0..1]; ... behavior Itab_is_zero: assumes Itab==0; requires \valid(Interp+(0..2)); assigns Interp[0..2]; ... */ Best regards, -- E tutto per oggi, a la prossima volta Virgile