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
Assigned Tovirgile 
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
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker