2021-01-18 18:53 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000735Frama-CKernelpublic2012-06-10 10:00
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000735: Pretty-printer and generated global annotations
DescriptionGenerated 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 Reproducewith 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003082

yakobowski (manager)

Seems to have been corrected at some point, between Carbon an Nitrogen.
+Notes

-Issue History
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
+Issue History