|View Issue Details [ Jump to Notes ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001761||Frama-C||Kernel > ACSL implementation||public||2014-04-23 17:49||2017-03-14 10:05|
|Assigned To||virgile|| |
|Product Version||Frama-C Neon-20140301|| |
|Target Version||Fixed in Version|| |
|Summary||0001761: Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires|
|Description||Here is a simple function foo where the assigns clause refers to the pointer a+n that is not
guarded by a \valid in the requires clause.
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 (or the Frama-C kernel) issued a warning about this discrepancy.|
|Additional Information||I posted this on the Frama-C mailing list. As far as I understood the discussion there it might be a feature request for the Frama-C kernel.
I noticed this problem when writing specs for code from a partner in the OpenETCS project.
|Tags||No tags attached.|