2021-01-26 19:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000690Frama-CPlug-in > slicingpublic2015-08-03 20:16
Reportersignoles 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionnot fixable 
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in Version 
Summary0000690: Slicing does not preserve some ACSL constructs
DescriptionThe slicer does not keep ACSL annotations if it does not understand them. This behavior may prevent to prove properties of the sliced program.
Steps To ReproduceConsider the following program:
==== a.c
int t[10];
void main(void) {
  /*@ loop invariant 0 <= i <= 10;
    @ loop invariant \forall integer k; 0 <= k < i ==> t[k] == 0;
    @ */
  for(int i = 0; i < 10; i++) t[i] = 0;
  /*@ assert t[0] == 0; */
}
====
Run it with:
$ frama-c -slice-assert main -slice-print a.c
The printed program forget the second loop invariant. Thus, for instance, plug-in WP cannot prove the final assertion anymore.

/* Generated by Frama-C */
int t[10] ;
void main(void)
{
  { int i ; i = 0;
    /*@ loop invariant (0 ? i) ? (i ? 10); */
    while (i < 10) { t[i] = 0; i ++; }
  }
  
  /*@ assert (t[0] ? 0); */ ;
  return;
}
TagsNo tags attached.
Attached Files

-Relationships
related to 0000090closedyakobowski Remove generated annotations from slicing results 
+Relationships

-Notes

~0001493

Anne (reporter)

The slicer cannot keep an annotation without knowing if it means something in the sliced program, either...
We thought that it was more correct to keep only the annotations when we are able to compute the data needed to evaluate it.
What else do you propose ?

Of course, the best would be for the slicer to "understand" every ACSL annotations :-D which means some enhancements in [src/logic/logic_interp.ml] I guess...

~0001494

signoles (manager)

Maybe somethink like: "if each C left-value of an ACSL annotation is still declared in the sliced program, keep it. Otherwise remove it". It could be refined by checking separately each conjunctive part of the formula.

If not the best, I think the result would be ok in most cases. Do you think it is a valid and feasible check?

~0001495

Anne (reporter)

This is feasible, but not valid, because the slicer is able to keep a variable declaration and slice the computations related to its value (when only its address is used for instance).

But I think that an over-approximation of the needed data might be feasible.
For instance, in your example, we could say that we need the value of i and t[..].
I don't really know what is the problem here : maybe the quantification ? We should ask Patrick...

~0001778

patrick (developer)

Last edited: 2011-04-14 09:04

Why the computation of the data needed by the annotaion fails ?
The explanation is: the [Zone.t] computation isn't fully implemented. It uses a conversion of ACSL terms into C terms them gets the locations from the C terms.
let loc =
  let exp = !Db.Properties.Interp.term_to_exp ~result:None t
  in !Db.From.find_deps_no_transitivity current_ki exp

Since k isn't a C lvalue, the conversion of k (and t[k]) fails.

A computation likes Db.From.find_deps_no_transitivity operating on acsl terms should be developed. It is a feature request of the slicer.

~0001779

patrick (developer)

Notice, when the computation of these locations fails, but are required by the slicing request, the slicer stops with a message asking for a feature request:

> frama-c -slice-loop-inv main -slice-print a.c
...
[kernel] State_builder.aborted because of unimplemented feature.
         Please send a feature request at http://bts.frama-c.com with:
         '[logic_interp] not an lvalue'.

~0003939

yakobowski (manager)

The code needed to reproduce note 3920 has been committed in commit 22722.
+Notes

-Issue History
Date Modified Username Field Change
2011-01-26 18:08 signoles New Issue
2011-01-26 18:08 signoles Status new => assigned
2011-01-26 18:08 signoles Assigned To => Anne
2011-02-14 10:55 Anne Note Added: 0001493
2011-02-14 11:28 signoles Note Added: 0001494
2011-02-14 11:48 Anne Note Added: 0001495
2011-04-11 17:29 Anne Assigned To Anne => patrick
2011-04-14 08:35 patrick Note Added: 0001778
2011-04-14 08:58 patrick Note Edited: 0001778
2011-04-14 09:01 patrick Note Edited: 0001778
2011-04-14 09:04 patrick Note Edited: 0001778
2011-04-14 09:37 patrick Note Added: 0001779
2011-04-14 09:38 patrick Severity major => feature
2012-05-16 18:26 signoles Assigned To patrick => yakobowski
2013-01-08 10:29 yakobowski Relationship added related to 0000090
2013-03-21 12:32 svn
2013-05-24 18:49 svn
2013-06-05 14:14 yakobowski Note Added: 0003939
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 831b5175
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 8246247c
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon 831b5175
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon 8246247c
2015-08-03 20:16 yakobowski Status assigned => closed
2015-08-03 20:16 yakobowski Resolution open => not fixable
+Issue History