--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on April 2014 ---
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.