--- layout: fc_discuss_archives title: Message 145 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Printing all global variables of a set of C files?



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.