Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.