--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on January 2014 ---
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