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)

Hello Jens,

2014-04-20 20:26 GMT+02:00 Gerlach, Jens <jens.gerlach at fokus.fraunhofer.de>:
> 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.

As you certainly know, this is normal, since the assigns clause is
correct: you never modify something outside of a[0..n].

> 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

I agree that there ought to be some "smell detectors" for
specifications that look like they might not express what the user
intended, though I'd rather see the kernel emit them. However, I think
that in this case, there is some potential for such a warning to
trigger a certain number of false positives in presence of
behaviors[1]. If we take for instance the following (purely
theoretical, I admit that I haven't seen something like that in real
code) contract:

/*@ requires \valid(a+(0 .. n-1));
       assigns a[0 .. n];
       behavior normal:
       assumes !P(a);
       assigns a[0 .. n-1];
       behavior one_past:
       assumes P(a);
       requires \valid(a+n);
       ensures a[n] == 42;
       ....
*/

In the general case, only cells from 0 to n-1 are required to be
valid, but behavior one_past asks for one more, and assigns a[n].
Thus, the general assigns clause must contain a[n].

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
[1] of course, one could restrict the warning to specifications
without behaviors.