Pretty-printer and generated global annotations
ID0000735: This issue was created automatically from Mantis Issue 735. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000735 | Frama-C | Kernel | public | 2011-02-22 | 2012-06-10 |
| Reporter | virgile | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
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.