Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000690Frama-CPlug-in > slicingpublic2011-01-26 18:082015-08-03 20:16
Reportersignoles 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionnot fixable 
PlatformOSOS Version
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 

-  Notes
(0001493)
Anne (reporter)
2011-02-14 10:55

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)
2011-02-14 11:28

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)
2011-02-14 11:48

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)
2011-04-14 08:35
edited on: 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)
2011-04-14 09:37

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)
2013-06-05 14:14

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

- 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-12 09:34 patrick Note Added: 0001727
2011-04-14 08:06 patrick Note Deleted: 0001727
2011-04-14 08:15 patrick Note Added: 0001776
2011-04-14 08:25 patrick Note Deleted: 0001776
2011-04-14 08:28 patrick Note Added: 0001777
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:32 patrick Note Deleted: 0001777
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
2012-05-16 18:29 yakobowski Relationship added related to 0001131
2012-07-15 20:02 yakobowski Relationship added related to 0001242
2012-07-27 14:55 signoles Relationship added related to 0001247
2013-01-08 10:29 yakobowski Relationship added related to 0000090
2013-03-21 12:32 svn Checkin
2013-05-24 18:49 svn Checkin
2013-06-05 14:14 yakobowski Note Added: 0003939
2015-08-03 20:16 yakobowski Status assigned => closed
2015-08-03 20:16 yakobowski Resolution open => not fixable


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker