Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000735Frama-CKernelpublic2011-02-22 18:412012-06-10 10:00
Assigned Tovirgile 
PlatformOSOS Version
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; } 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.c -print returns a C file without the lemma foo.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
yakobowski (manager)
2012-06-09 23:52

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

- 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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker