Frama-C Bug Tracking System - Frama-C
View Issue Details
0000257Frama-CKernelpublic2009-09-29 17:242014-02-12 16:56
Jonathan-Christofer Demay 
pascal 
normalminoralways
closedfixed 
Frama-C Beryllium-20090901 
Frama-C Boron-20100401 
0000257: get_varinfo not exported in src/ai/base.mli
get_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
No tags attached.
Issue History
2009-09-29 17:24Jonathan-Christofer DemayNew Issue
2009-09-30 09:34signolesStatusnew => assigned
2009-09-30 09:34signolesAssigned To => pascal
2009-09-30 09:44pascalNote Added: 0000424
2009-09-30 10:00svnCheckin
2009-09-30 10:00svnStatusassigned => resolved
2009-09-30 10:00svnResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron

Notes
(0000424)
pascal   
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