0000735: Pretty-printer and generated global annotations

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

Notes
(0003082) 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