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

[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)



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