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?

  • Subject: [Frama-c-discuss] Printing all global variables of a set of C files?
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Mon, 30 Sep 2013 10:15:32 +0000
  • In-reply-to: <CAC3Lx=YHQsCeWEP0q7eZbfz1S9OS2625Lrk4BR5-MVF+jXZw+g@mail.gmail.com>
  • References: <CAC3Lx=YHQsCeWEP0q7eZbfz1S9OS2625Lrk4BR5-MVF+jXZw+g@mail.gmail.com>
Dear David,

The script below, run with the following command line, should work:
frama-c -load-script d\:/cygwin/gena/pgv.ml -printglobalvars foo.c

HTH
D.


(* *************************************************************** *)
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 main () =
Globals.Vars.iter (fun vi ii -> 
	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 
)

let () = Db.Main.extend main
(* *************************************************************** *)



> -----Message d'origine-----
> De?: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-
> discuss-bounces at lists.gforge.inria.fr] De la part de David MENTRE
> Envoy??: lundi 30 septembre 2013 11:29
> ??: Frama-C public discussion
> Objet?: [Frama-c-discuss] Printing all global variables of a set of C
> files?
> 
> Hello,
> 
> Does anybody know how to print all the global variables of a set of C
> files?
> 
> I would like to print basic information:
>   * Variable name;
> 
>   * Definition location (file / line number);
> 
>   * Variable type;
> 
>   * (Optionally) Initial value at definition point.
> 
> I am pretty sure one could write a plug-in to do that but I don't know
> how to write plug-ins.
> 
> Does anybody know a way to use Frama-C Fluorine or one of its plug-in
> to get all or part of above information (maybe debug option of a plug-
> in)? I don't mind doing a few greps or other command line filtering if
> needed.
> 
> I tried to use frama-c-gui for that purpose but there are some
> pitfalls:
>   * This is not very automated, one needs to click on each .c file to
> see all the variables;
> 
>   * There is no distinction between locally (to a file) defined
> variables and "extern" ones. One need to refer to the C source file to
> get this info from the GUI;
> 
>   * Strangely enough, some variables where missing from the normalized
> program window or the list of global objects of the C file, even if
> this variable is defined in the C source code;
> 
>   * Only 21 global objects are displayed in the normalized program
> window.
> 
> Best regards,
> david
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss