View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000735 | Frama-C | Kernel | public | 2011-02-22 18:41 | 2012-06-10 10:00 | ||||
Reporter | virgile | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20110201 | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000735: Pretty-printer and generated global annotations | ||||||||
Description | Generated global annotations are supposed not to be in the AST and get pretty-printed separately, when we have passed types and global variables definitions. However, currently if there is no function declaration, they are simply ignored. More generally, current handling of global annotations seems wacky at best. | ||||||||
Steps To Reproduce | with test.c: int main () { return 0; } test.ml: open Cil_types let foo () = Globals.Annotations.add_generated (Dlemma("foo",false,[],[],Logic_const.ptrue,Cil_datatype.Location.unknown)) let () = Db.Main.extend foo frama-c -load-script test.ml test.c -print returns a C file without the lemma foo. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2012-06-09 23:52 |
Seems to have been corrected at some point, between Carbon an Nitrogen. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-02-22 18:41 | virgile | New Issue | |
2011-02-22 18:41 | virgile | Status | new => assigned |
2011-02-22 18:41 | virgile | Assigned To | => virgile |
2012-06-09 23:52 | yakobowski | Note Added: 0003082 | |
2012-06-09 23:52 | yakobowski | Status | assigned => closed |
2012-06-09 23:52 | yakobowski | Resolution | open => fixed |
2012-06-10 10:00 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |