--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] two-dimensional array requires clause



Hello,

Le 28/01/2014 00:39, Dragan a ?crit :
> I'd like to know how to I write requires clause for two-dimensional arrays.

I would write it like that:
---------------------
/*@ requires \forall integer i; 0 <= i < n ==>
                  (\forall integer j; 0 <= j < n ==>
                     (\valid(&a[i][j]) && a[i][j] >= 0));
// or
     requires \valid(&(a[0..n-1][0..n-1]));

     requires n == 5;
  */
void f(int a[5][5], int n)
{
   a[4][4] = 1;
}

void main(void)
{
   int a[5][5] = { {0, }, };

   f(a, 5);
}
---------------------

"frama-c-gui -wp -wp-rte 2d_req.c" proves all predicates but the RTE 
assert on "a[4][4] = 1" (why?).

"frama-c-gui -val -slevel 100 2d_req.c" proves all but the quantified 
predicate in f()'s contract (but this is expected).

> Is there is some new function similar to \valid()?

"\valid(&(a[0..n-1][0..n-1]))"?

Best regards,
david