Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000448Frama-CPlug-in > slicingpublic2010-04-13 08:372014-02-12 16:55
Reporterdpariente 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000448: invariant with quantifier not kept in computed slice
DescriptionOn the following code:

void L (float u,int nn, float dabs[], float *y)
{ int ii;
 /*@ loop invariant (\forall integer k; 0<=k<ii ==> u<=dabs[k]); */
    for (ii = nn-2; ii >= 0; ii--) *y = u - dabs[ii+1] * 2.0;
//@slice pragma expr *y;
}

analyzed with:
frama-c -slicing-keep-annotations -slice-pragma L -slice-print -ocode L_sliced.c -main L -lib-entry l.c

the computed slice does not contain the invariant.

(Please note that the invariant annotation is not relevant nor provable, but just illustrates the problem met)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000767)
Anne (reporter)
2010-04-14 12:48

The loop invariant is now in the slice when the -slicing-keep-annotations option is used. Maybe it should also be kept without the option, but the data needed by dabs[k], with k being a logical variable, is difficult to compute.
(0000769)
Anne (reporter)
2010-04-16 08:44

Fixed in rev 8438 : keeping the annotation
without option -slicing-keep-annotations is another feature request.

- Issue History
Date Modified Username Field Change
2010-04-13 08:37 dpariente New Issue
2010-04-13 08:37 dpariente Status new => assigned
2010-04-13 08:37 dpariente Assigned To => Anne
2010-04-13 17:44 svn Checkin
2010-04-14 10:29 svn Checkin
2010-04-14 11:52 svn Checkin
2010-04-14 12:48 Anne Note Added: 0000767
2010-04-16 08:44 Anne Note Added: 0000769
2010-04-16 08:44 Anne Status assigned => resolved
2010-04-16 08:44 Anne Fixed in Version => Frama-C svn, precise the release id
2010-04-16 08:44 Anne Resolution open => fixed
2010-04-29 08:45 svn Checkin
2010-04-29 08:46 svn Checkin
2010-12-10 15:40 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker