Frama-C Bug Tracking System - Frama-C
View Issue Details
0000679Frama-CPlug-in > slicingpublic2011-01-19 17:042014-02-12 16:54
patrick 
Anne 
normalcrashhave not tried
closedfixed 
 
Frama-C Oxygen-20120901 
0000679: untypable ACSL in a sliced program containing \at(p,label) when the label was removed
bug when a code annotation refers to a label and the label is removed into the sliced program.
===== 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
No tags attached.
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:58svnCheckin
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

Notes
(0001402)
patrick   
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.
(0002427)
Anne   
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/annot.ml) could include the nodes of the labels in its result.
(0002434)
patrick   
2011-10-28 09:36   
As there are some extract functions into cil.ml, I can add a function Cil.extract_labels_from_annot: Cil_types.code_annotation -> Cil_datatype.Logic_label.Set.t From it, it is possible to build a function extracting C stmt : Cil.extract_stmts_from_labels Cil_datatype.Logic_label.Set.t -> Cil_datatype.Stmt.Set.t Anne, will it be ok for you ?
(0002435)
patrick   
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.
(0002437)
patrick   
2011-10-28 11:00   
The new field lbl has to be used into [src/pdg/annot.ml]...
(0002438)
patrick   
2011-10-28 11:23   
Bug fixed Sending src/pdg/annot.ml Adding tests/slicing/bts679.i Adding tests/slicing/oracle/bts679.res.oracle Committed revision 15974.
(0002445)
Anne   
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).
(0002446)
Anne   
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.
(0002447)
Anne   
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...
(0002448)
Anne   
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]...
(0002451)
patrick   
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.