2021-02-27 11:14 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001136Frama-CKernelpublic2014-02-12 16:59
ReporterAnne 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001136: [Globals.Vars.get_astinfo] doesn't work
Description[Globals.Vars.get_astinfo] compares variable names instead of using [Varinfo.equal], so it gives erroneous results.
Additional Informationint f (int x) { return x; }
int g (int x) { return x; }
int h (int x) { return x; }

$ frama-c -load-script script.ml toto.c

found variable vid:363 formal in f
found variable vid:367 formal in g
found variable vid:371 formal in h
[do_v] vid:371 formal in f
[do_v] vid:367 formal in f
[do_v] vid:363 formal in f
TagsNo tags attached.
Attached Files
  • ? file icon script.ml (984 bytes) 2012-03-27 14:12 -
    let get_named_variables name =
      let add_kf_vars kf vars =
        try 
          let v = Globals.Vars.find_from_astinfo name (Cil_types.VFormal kf) in
          Format.printf "found variable vid:%d formal in %a@."
            v.Cil_types.vid Cil_datatype.Kf.pretty kf;
          v::vars
        with Not_found -> vars
      in
      let vars = Globals.Functions.fold add_kf_vars [] in
        vars
    
    let main () =
      Ast.compute ();
      let vars = get_named_variables "x" in
      let do_v v =
        let pp_kind fmt kind = match kind with
          | Cil_types.VGlobal -> Format.fprintf fmt "global"
          | Cil_types.VFormal kf -> 
              Format.fprintf fmt "formal in %a" Cil_datatype.Kf.pretty kf
          | Cil_types.VLocal kf -> 
              Format.fprintf fmt "local in %a" Cil_datatype.Kf.pretty kf
        in
        let _, kind = Globals.Vars.get_astinfo v in
          Format.printf "[do_v] vid:%d %a@."  v.Cil_types.vid 
           (* Cil_datatype.Localisation.pretty *) pp_kind kind
      in List.iter do_v vars
    
    let () = Db.Main.extend main
    
    ? file icon script.ml (984 bytes) 2012-03-27 14:12 +

-Relationships
+Relationships

-Notes

~0004707

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-03-27 14:12 Anne New Issue
2012-03-27 14:12 Anne File Added: script.ml
2012-03-27 15:58 virgile Status new => assigned
2012-03-27 15:58 virgile Assigned To => virgile
2012-03-30 17:54 svn
2012-03-30 17:54 svn Status assigned => resolved
2012-03-30 17:54 svn Resolution open => fixed
2012-04-24 11:24 pascal Status resolved => feedback
2012-04-24 11:24 pascal Resolution fixed => reopened
2012-06-16 22:18 yakobowski Status feedback => resolved
2012-06-16 22:18 yakobowski Resolution reopened => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master 4663401c
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 4663401c
2014-02-12 16:59 Note Added: 0004707
2014-02-12 16:59 Status closed => resolved
+Issue History