Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001761Frama-CKernel > ACSL implementationpublic2014-04-23 17:492017-03-14 10:05
Reporterjens 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001761: Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires
DescriptionHere 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 InformationI 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006386)
jens (reporter)
2017-03-14 10:05

The issue is present also in Silicon.

- Issue History
Date Modified Username Field Change
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 - 2017 MantisBT Team
Powered by Mantis Bugtracker