--- layout: fc_discuss_archives title: Message 145 from Frama-C-discuss on September 2013 ---
Hello Anne, Dillon and St?phane, 2013/9/30 Pariente Dillon <Dillon.Pariente at dassault-aviation.com>: > The script below, run with the following command line, should work: > frama-c -load-script d\:/cygwin/gena/pgv.ml -printglobalvars foo.c Thanks a lot! This -load-script option is very convenient! I have changed your script to keep only the globally visible variables at their definition point (i.e. no "extern" neither "static" variables"), here is my version: (* **************************************** *) open Cil_types module Param = Plugin.Register (struct let name = "PGV" let shortname = "pgv" let help = "" end) open Param module PrintGlobalVars = Bool(struct let option_name = "-printglobalvars" let help = "prints global vars." let default = false end) let globally_visible_definition vstorage = match vstorage with | NoStorage -> true | Static -> false | Register -> true | Extern -> false let main () = Globals.Vars.iter (fun vi ii -> if globally_visible_definition vi.vstorage then begin Format.printf "@.Global Var: %s : %a @ %a" vi.vname Printer.pp_location vi.vdecl Printer.pp_typ vi.vtype; if (PrintGlobalVars.get()) then match ii.init with | None -> Format.printf "@." | Some info -> Format.printf " = %a at ." Printer.pp_init info end ) let () = Db.Main.extend main (* **************************************** *) Some remarks: * The list of found variables is correct, i.e. all my global variables are in the list produced by the script; * If I try to keep only the definition points, where "vi.vdefined = true" as shown on Anne's page (https://anne.pacalet.fr/Notes/outils/frama-c/scripts/#index3h2), but some variables are missing; * I don't need to use "Rmtmps.keepUnused := true" trick, as I am already seeing all my variables; * Some definition location refer to the foo.h instead of the foo.c file. I checked for some of those variables: the foo.h file correctly defines the variable as "extern" (extern int v;) and the foo.c file defines the variable (int v;). Why the foo.h file is referenced? I also observe the same behaviour for a global variable referenced into another C file (using "extern int v" in a function f()), the location printed is this later location (I would have expected the former definition location). * I have a variable "v" erroneously defined in two C files (a.c and b.c): what is the expected behaviour of a C compiler and Frama-C in such a case? As is, this plug-in is far from giving a perfect result[1] but it is very useful to check my manually made list and spotted some forgotten variables (and it is much quicker! :-) ). Thanks a lot! Best regards, david [1] No intended critic of your script Dillon, but rather open questions on Frama-C behaviour.