Frama-C Bug Tracking System - Frama-C
View Issue Details
0001025Frama-CKernelpublic2011-11-21 11:452014-02-12 16:58
fgarnier 
yakobowski 
lowminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Oxygen-20120901 
0001025: Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
Hello, I am developing some Frama-c plugin to extract some counter automata based models of C programs, and I am currently developing this plugin using the Carbon-20110201 release. To generate our model, I am using some graph traversal algorithm on the Control flow graph computed by Cil, and I do perform some analysis on the the arguments of the instructions. At some point, I do traverse a "Skip" type instruction, and the value contained in the the Cil_types.location argument is : "In file : Cabs2cil_start, from line 0 col -1 to line 0 col -1." The file Cabs2cil_start appears to be some Framac file, issued in the carbon version. This is strange, because others instruction that contains location positions, used to contain value that deal with the analyzed C source code -- And I was expecting to get such a value. After some time spent on the Mantis BTS, I noticed that some issues were the name "Cabs2cil_start" appeared, were solved, but I can't figure out if this will solve the problem I get. Maybe I won't get this problem anymore, when I will migrate from Carbon to the new Nitrogen version, but I prefer to point this strange thing to you. I have two extra questions : Concerning the Skip instruction, does it mean that the control goes through the statement without performing any operation ? Is it still worth reporting bugs on the Carbon version of Frama-C ? Best regards, Florent Garnier.
The Skip "instruction" is defined in the file Cil_types.ml. and stmtkind = | Instr of instr (** An instruction that does not contain control flow. Control * implicitly falls through. *) | Return of exp option * location (** The return statement. This is a leaf in the CFG. *) [...] and instr = Set of lval * exp * location (** An assignment. A cast is present if the exp has different type from lval *) [...] | Skip of location | Code_annot of code_annotation * location
No tags attached.
tgz debug.tgz (3,537) 2011-11-22 11:49
https://bts.frama-c.com/file_download.php?file_id=298&type=bug
? vis.ml (627) 2011-11-25 10:58
https://bts.frama-c.com/file_download.php?file_id=299&type=bug
tgz Debug_plugin.tgz (9,211) 2011-11-28 15:59
https://bts.frama-c.com/file_download.php?file_id=301&type=bug
Issue History
2011-11-21 11:45fgarnierNew Issue
2011-11-21 14:45signolesStatusnew => assigned
2011-11-21 14:45signolesAssigned To => virgile
2011-11-21 15:29fgarnierNote Added: 0002492
2011-11-21 20:51monateNote Added: 0002496
2011-11-21 23:34yakobowskiNote Added: 0002497
2011-11-22 11:48fgarnierNote Added: 0002500
2011-11-22 11:49fgarnierFile Added: debug.tgz
2011-11-22 11:50fgarnierNote Added: 0002501
2011-11-24 12:14yakobowskiNote Added: 0002502
2011-11-24 12:15yakobowskiStatusassigned => confirmed
2011-11-24 12:48yakobowskiNote Added: 0002503
2011-11-25 09:49yakobowskiNote Deleted: 0002503
2011-11-25 09:51yakobowskiNote Edited: 0002502
2011-11-25 10:57yakobowskiNote Added: 0002504
2011-11-25 10:58yakobowskiFile Added: vis.ml
2011-11-25 10:58yakobowskiStatusconfirmed => feedback
2011-11-25 14:50fgarnierNote Added: 0002505
2011-11-25 15:13yakobowskiNote Added: 0002506
2011-11-28 15:59fgarnierFile Added: Debug_plugin.tgz
2011-11-28 16:14fgarnierNote Added: 0002509
2011-11-28 16:16fgarnierNote Added: 0002510
2011-11-28 16:25fgarnierNote Added: 0002511
2012-01-18 23:29yakobowskiStatusfeedback => assigned
2012-01-18 23:29yakobowskiAssigned Tovirgile => yakobowski
2012-02-08 21:38yakobowskiNote Added: 0002678
2012-02-08 21:40yakobowskiPrioritynormal => low
2012-02-08 21:40yakobowskiStatusassigned => confirmed
2012-02-08 21:40yakobowskiSummaryUnsound lexing position --Cil_types.location-- given as argument of the Skip(loc) -- type : Cil_types.instr, in the Carbon-2011 => Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
2012-02-08 21:52yakobowskiNote Added: 0002679
2012-02-08 22:16svnCheckin
2012-02-08 22:16svnStatusconfirmed => resolved
2012-02-08 22:16svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58yakobowskiNote Added: 0004680
2014-02-12 16:58yakobowskiStatusclosed => resolved

Notes
(0002492)
fgarnier   
2011-11-21 15:29   
I did port my current implementation of the plugin so that it compiles and run using the nitrogen version of Frama-c. I still have the same problem. Best regards, Florent.
(0002496)
monate   
2011-11-21 20:51   
Hi, Thanks for your report. Could you post the C source code that leads to such inconsistant locations?
(0002497)
yakobowski   
2011-11-21 23:34   
Hi Florent; Regarding your other questions - it is still worth reporting bugs in Carbon, but reproducing them on Nitrogen beforehand would be a strong plus; - the Skip instruction of Cil is supposed to be a Nop. Neither the control-flow nor the memory state are changed.
(0002500)
fgarnier   
2011-11-22 11:48   
Thank you for your fast answers ! I have to correct something concerning the "bug" under the Nitrogen Version, I think I get confused at some point while testing the plugin after I made it compliant with the Nitrogen release -- I think I launched frama-c carbon from a shell in which my environment variables weren't yet updated, sorry for that. By the way, I don't get this "Cabs2cil_start, from line 0 col -1 to line 0 col -1." anymore, while pretty printing location information under Nitrogen. I either get : In statement :42, skipping to statement 43, located at In file : , from line 0 col -1 to line 0 col -1. or In statement :57, skipping to statement 58, located at In file : examples/veridyc/main.c, from line 25 col 8 to line 25 col 35. which looks fine. I bet in this case that "from line 0 col -1 to line 0 col -1." correspond to a statment added by Cil, that does not correspond to a real source file location. I am uploading the C-source file of the example that generates the aforementioned behavior under the Carbon release. Best regards, Florent.
(0002501)
fgarnier   
2011-11-22 11:50   
ps : The file that generates this problem under the carbon verion is : main.c . Florent.
(0002502)
yakobowski   
2011-11-24 12:14   
(edited on: 2011-11-25 09:51)
Hi Florent, I've partly reproduced the bug. Those skip statements are introduced inside "undefined sequences" compound statements. It seems that Cil replaces some subparts of those "undefined sequences", and replaces them by Skip. However, with my visitor, all statements have a correct location, even the Skip ones. Does your plugin use a copy visitor somewhere?
(0002504)
yakobowski   
2011-11-25 10:57   
Ok, after a careful analysis, the Skip are here for a good reason. In a line such as "if (strstr(line, "put") == line)", there is a possible unspecified sequence, because line is used both in the call and in the comparison. The Skip are used to encode which expressions overlap. So the generated code is in fact { // Unspecified sequence tmp = strstr(line, "put"); // Skip statement, that carries the fact that 'line' is used by a second statement later } if (tmp == line) {...} It is essentially equivalent to {// Unspecified sequence tmp1 = strstr(line, "put"); tmp2 = tmp1 == line; } if (tmp2) In this form, the unspecified sequence is much more obvious, but the 'if' is less legible, and there is one more temporary. Back to the original point, can you reproduce the bug on Nitrogen without your plugin? I'm using the visitor attached to see the locations on the Skip.
(0002505)
fgarnier   
2011-11-25 14:50   
Hi Boris, Since I migrated under Frama-c Nitrogen, I have not been concerned again with the problem I first described. I fetched the visitor you uploaded, I will try to see what happen if I use the it. I am using inplace visitors, and I only perform reading operation on the AST. " class flatac_visitor (prj : Project.t ) = object (self) inherit Visitor.generic_frama_c_visitor (prj) (Cil.inplace_visit()) " I wrote a simpler debugging visitor that showed me the same problem under Carbon -- In order to better locate the source of my issue, however, it seems that everything is correct under Nitrogen for both my visitors. I will reinstall the Carbon version at home this week-end to check how your visitor behaves under Carbon. Bests, Florent. ps : Thank you for your support !
(0002506)
yakobowski   
2011-11-25 15:13   
Hi Florent ! Actually I was refering to your note 0002500, were you mentioned you sometimes still got messages like "In statement :42, skipping to statement 43, located at In file : , from line 0 col -1 to line 0 col -1." The final location corresponds to Cil_datatype.Location.unknown, which we try to eradicate from our ast. If you can get this message on Nitrogen with an unmodified Ast (and your visitor seems okay regarding this point), we are definetely interested. And no need to test this on Carbon.
(0002509)
fgarnier   
2011-11-28 16:14   
Hi Boris, I uploaded some small plugin that performs the traversal of the control flow graph computed thanks to the primitives of the Cfg module, using the successor relation defined in the Cil_types.stmt type definition. I don't get the problem using your visitor, which performs well. So, maybe there is rather an issue with the Cfg --prepareCfg, computeCfginfo-- than than something else. I included it as well in the tarball, so that you can compare the output of both visitors. I still have the problem when I use To be short : The plugin only performs a graph traversal of the Cfg computed using Frama-c, then builds an instance of the class cautomaton defined in the file cautomata.ml. I do print the location informations in the method add_trans_from_stmt of the class panalyse defined in the file c2cautomatanalys.ml. I lacked time to write a shorter plugin that displays the problem, however, I will be able to do so, if it helps you. Best regards, Florent.
(0002510)
fgarnier   
2011-11-28 16:16   
The pluging is a dynamic one and should compile and install using make && make install. Bests, Florent.
(0002511)
fgarnier   
2011-11-28 16:25   
The file main.c provided in the debug.tgz tarball shows the issue. Florent.
(0002678)
yakobowski   
2012-02-08 21:38   
Hi Florent, Sorry for having left this bug dormant so long. As you thought, the issue lies in the cfg normalization function. More precisely, Cfg.prepareCFG uses Location.unknown for the labels it inserts when removing 'continue', 'break' or 'switch' instructions. This can be fixed, but there is no good location to use: those statements are not part of the original source, and do not really correspond to an original statement either. Also, you might possibly avoid calling Cfg.prepareCFG yourself entirely. Indeed, Frama-C "-simplify-cfg" option does essentially the same thing. For some reason, it also inserts less useless labels (hence less Skip), which results in a cleaner AST. Hope this helps
(0002679)
yakobowski   
2012-02-08 21:52   
Ok, I have found some good locations, that will hopefully not interfere with pre-existing ones. This bug will thus be fixed in the next version of Frama-C. If it is useful, I can send you the patch privately.
(0004680)
yakobowski   
2014-02-12 16:58   
Fix committed to stable/neon branch.