Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Sun, 20 Apr 2014 18:26:46 +0000
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