| 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 | |
| Platform | | OS | | OS Version | |
| 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 | |
|
Relationships 
Relationships