|Anonymous | Login | Signup for a new account||2018-01-23 08:54 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|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|
|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.|
|2014-04-23 17:49||jens||New Issue|
|2014-04-24 10:35||signoles||Assigned To||=> virgile|
|2014-04-24 10:35||signoles||Status||new => assigned|
|2015-07-17 09:09||signoles||Category||Kernel => Kernel > ACSL implementation|
|2017-03-14 10:05||jens||Note Added: 0006386|
|Copyright © 2000 - 2018 MantisBT Team|