Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000257Frama-CKernelpublic2009-09-29 17:242014-02-12 16:56
ReporterJonathan-Christofer Demay 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000257: get_varinfo not exported in src/ai/base.mli
Descriptionget_varinfo (create_varinfo but the other way around) is defined in src/ai/base.ml (essentially because of me ^^;) but not exported in src/ai/base.mli

diff -Naur frama-c-Beryllium-20090601-beta1-orig/src/ai/base.mli frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.mli
--- frama-c-Beryllium-20090601-beta1-orig/src/ai/base.mli 2009-05-05 14:29:35.000000000 +0000
+++ frama-c-Beryllium-20090601-beta1-ptch/src/ai/base.mli 2009-07-12 17:09:54.000000000 +0000
@@ -61,6 +61,7 @@
 val is_block_local: t -> Cil_types.block -> bool
 val is_hidden_variable : t -> bool
 val validity_from_type : Cil_types.varinfo -> validity
+val get_varinfo : t -> Cil_types.varinfo
 val create_varinfo : Cil_types.varinfo -> t
 val create_logic : Cil_types.varinfo -> validity -> t
 val create_initialized : Cil_types.varinfo -> validity -> t
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000424)
pascal (reporter)
2009-09-30 09:44

Ok.
To work around the problem, note that the type Base.t is private: you are not allowed to build objects of this type, but you can inspect them by pattern matching. Therefore, it is possible to implement the function get_varinfo in your own plug-in by writing:

let get_varinfo t =
  match t with
  | Base.Var (t,_) | Base.Initialized_Var (t,_) -> t
  | _ -> assert false

- Issue History
Date Modified Username Field Change
2009-09-29 17:24 Jonathan-Christofer Demay New Issue
2009-09-30 09:34 signoles Status new => assigned
2009-09-30 09:34 signoles Assigned To => pascal
2009-09-30 09:44 pascal Note Added: 0000424
2009-09-30 10:00 svn Checkin
2009-09-30 10:00 svn Status assigned => resolved
2009-09-30 10:00 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker