--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on April 2014 ---
Here is a simple function foo that sets all elements of an array to zero. /*@ requires \valid(a + (0..n-1)); assigns a[0..n]; // should be a[0..n-1] */ void foo(int* a, unsigned int n) { /*@ loop invariant 0 <= i <= n; loop assigns i, a[0..n]; // should be a[0..n-1]; loop variant n-i; */ for(unsigned int i = 0; i < n; ++i) a[i] = 0; } Using the command line frama-c-gui.byte -wp -wp-rte -wp-model Typed+ref -wp-timeout 10 -wp-prover alt-ergo -wp-out loop_assigns.wp loop_assigns.c I can see that all proof obligations are discharged by either Qed or Alt-Ergo. My question is about the assigns clause which refers to all offsets of a in the range [0..n]. (Note that I use the same range in the loop assigns clause.) The precondition, however, only states that array offsets in the range [0..n-1] are valid. I think I would prefer if WP issued a warning about this discrepancy. What do you think? Regards Jens