Frama-C Bug Tracking System - Frama-C
View Issue Details
0000679Frama-CPlug-in > slicingpublic2011-01-19 17:042014-02-12 16:54
Assigned ToAnne 
PrioritynormalSeveritycrashReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000679: untypable ACSL in a sliced program containing \at(p,label) when the label was removed
Descriptionbug when a code annotation refers to a label and the label is removed into the sliced program.

Additional Information===== bug.c =====
void f(void) { return; }
int X = 1 ;
int main(void) {
 call: f();
  //@ assert X == \at(X,call);
  return X;

$frama-c bug.c -slice-return main -then-on "Slicing export" -print -ocode sliced_bug.c
[kernel] failure: Cannot find label for \at

$ frama-c sliced_bug.c
TagsNo tags attached.
Attached Files

2011-01-21 11:16   
A first action fixing the bug can be done:
1) filter out code annotations containing \at(e,L) constructs when the statement labeled by L is filtered out

A better alternative could be:
2a) filter out code annotations containing \at(e,L) constructs when control dependency of the statement labeled by L is not preserved (control mark=bottom).
2b) do not filter out a labeled statement when its control dependency is preserved : if the statement effects are not preserved then replace the statement by a skip statement otherwise keep the statement as it is.
2011-10-27 15:54   
I think that the easiest way to fix this problem is to change [!Db.Properties.Interp.To_zone.from_stmt_annot] in order that it also returns the user labels needed by the annotation so that [find_code_annot_nodes] (in src/pdg/ could include the nodes of the labels in its result.
2011-10-28 09:36   
As there are some extract functions into, I can add a function
  Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t

From it, it is possible to build a function extracting C stmt :
 Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t

Anne, will it be ok for you ?
2011-10-28 10:58   
In fact I modified the type t_decl returned by most of the functions of To_zone.from_xxxx. It was Cil_datatype.Varinfo.Set.t.
t_decl contents a field var -> the previous Cil_datatype.Varinfo.Set.t,
and a field lbl:Cil_datatype.Stmt.Set.t -> the statement referenced labels of the At() constructions.
2011-10-28 11:00   
The new field lbl has to be used into [src/pdg/]...
2011-10-28 11:23   
Bug fixed

Sending src/pdg/
Adding tests/slicing/bts679.i
Adding tests/slicing/oracle/

Committed revision 15974.
2011-11-03 06:41   
Well, I think that the bug is still there :

int X = 1 ;
int main(void) {
  int y;
L: y = 0;
  //@ assert X == \at(X,L);
  return X;

$ frama-c -slice-assert main toto.c -slicing-debug 2
[slicing] [SlicingTransform.Visibility.label_visible] label L: is invisible
[slicing] [SlicingTransform.Visibility.annotation_visible] -> yes
[kernel] failure: Cannot find label for \at

and this is because the label and the statement are two separate things in the PDG. So it would be better if [Db.Properties.Interp.To_zone.from_stmt_annot] could return real labels instead of statements. (set of pairs [(stmt * label)] would be perfect).
2011-11-03 11:28   
Well, finally, many things about labels are missing: for instance, the PDG only has nodes for labels that are used for jumps, and high level function to find labels in PDG or to select them in slicing are also missing... I try to add this as soon as possible.
2011-11-03 13:14   
The example above is now in [tests/slicing/bts679b.i].

It is working in rev16020 (had finally to also change [slicingCommand] since [pdg/annot] seems to be not used in that context).

Anyway, the slicing could be better: I don't know why [y=0] is selected as [spare] instead of being sliced away...
2011-11-03 17:01   
@Patrick: sorry ! I didn't succeed to fix the problem. Our idea was good: changing [select_stmt_zone] by [select_stmt_zone_internal] at the end of [select_ZoneAnnot_zones_decl_vars] solve the problem above, but some other tests (like [tests/slicing/bts341.c] for instance) don't work anymore then.

I think that the main problem is that, on one hand, we build requests to slice for an annotation in [slicingCmd] but on the other hand, we use PDG [find_code_annot_nodes] in [slicingTransform] to decide if the annotation is visible at the end.
I guess that the selections are probably not the same (as they should be!), but I haven't found why :-(

We probably tests the visibility of two many nodes for the control dependencies in [find_code_annot_nodes]...
2011-11-04 08:45   
The remaining problem is that some slicing results have too much [spare] selections. This isn't directly due to the previous changes.

That comes from [slicingCmd] and the interface of To_zone.from_xxxx functions. These functions return couples of [Zones*Stmt], and [slicingCmd] selects the ctrl of theses [Stmt], and their integrality as [spare].
To solve the remaining problem, they should return [Zones*Label] instead and [slicingCmd] should select the ctrl of theses [Label], and their integrality as [spare].

This work can be considered as another feature wished.
The initial bug is now fixed.

Issue History
2011-01-19 17:04patrickNew Issue
2011-01-19 17:04patrickStatusnew => assigned
2011-01-19 17:04patrickAssigned To => Anne
2011-01-21 11:16patrickNote Added: 0001402
2011-04-14 09:50patrickSeverityminor => crash
2011-10-27 15:54AnneNote Added: 0002427
2011-10-28 09:36patrickNote Added: 0002434
2011-10-28 10:58patrickNote Added: 0002435
2011-10-28 10:58svn
2011-10-28 11:00patrickNote Added: 0002437
2011-10-28 11:23patrickNote Added: 0002438
2011-11-03 06:41AnneNote Added: 0002445
2011-11-03 11:28AnneNote Added: 0002446
2011-11-03 13:14AnneNote Added: 0002447
2011-11-03 17:01AnneNote Added: 0002448
2011-11-04 08:45patrickNote Added: 0002451
2011-11-04 08:46patrickStatusassigned => resolved
2011-11-04 08:46patrickResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:12patrickSource_changeset_attached => framac master f82bc43b
2014-02-12 16:54patrickSource_changeset_attached => framac stable/neon f82bc43b