# 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*: virgile.prevosto at m4x.org (Virgile Prevosto)*Date*: Tue, 22 Apr 2014 09:37:52 +0200*In-reply-to*: <A246AA9F-4050-4278-A52E-9E9CDC45AD7B@fokus.fraunhofer.de>*References*: <A246AA9F-4050-4278-A52E-9E9CDC45AD7B@fokus.fraunhofer.de>

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.

**Follow-Ups**:**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

**References**:**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)***From:*jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)

- Prev by Date:
**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)** - Next by Date:
**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)** - Previous by thread:
**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)** - Next by thread:
**[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)** - Index(es):