Frama-C Bug Tracking System - Frama-C
View Issue Details
0000448Frama-CPlug-in > slicingpublic2010-04-13 08:372014-02-12 16:55
Frama-C GIT, precise the release id 
Frama-C Carbon-20101201-beta1 
0000448: invariant with quantifier not kept in computed slice
On 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)
No tags attached.
Issue History
2010-04-13 08:37dparienteNew Issue
2010-04-13 08:37dparienteStatusnew => assigned
2010-04-13 08:37dparienteAssigned To => Anne
2010-04-13 17:44svnCheckin
2010-04-14 10:29svnCheckin
2010-04-14 11:52svnCheckin
2010-04-14 12:48AnneNote Added: 0000767
2010-04-16 08:44AnneNote Added: 0000769
2010-04-16 08:44AnneStatusassigned => resolved
2010-04-16 08:44AnneFixed in Version => Frama-C svn, precise the release id
2010-04-16 08:44AnneResolutionopen => fixed
2010-04-29 08:45svnCheckin
2010-04-29 08:46svnCheckin
2010-12-10 15:40signolesFixed in VersionFrama-C GIT, precise the release id => Frama-C Carbon-20101201-beta1
2010-12-17 19:38signolesStatusresolved => closed

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.
2010-04-16 08:44   
Fixed in rev 8438 : keeping the annotation
without option -slicing-keep-annotations is another feature request.