Search code examples
ocamlframa-c

Frama-C: how to get only line number

I'm developping a plugin in frama-c and I want to get line number in source code. In this little script for example:

open Cil_types
open Cil_types
open Cil_datatype
let print_loc kf =             
let locals = Kernel_function.get_locals kf in 
   List.iter (fun vi -> 
      let line =  Cil_datatype.Location.pretty_line Format.sprintf "%a" Printer.pp_location vi.vdecl in
      Format.printf "Line %a: %a %s@." 
      Printer.pp_location vi.vdecl Printer.pp_typ vi.vtype vi.vname
   ) locals

let () =
Db.Main.extend (fun () ->
  Format.printf "Printing all local vars...@.";
  let fun_name = "main" in
  let kf = Globals.Functions.find_by_name fun_name in
  print_loc kf;
  Format.printf "done!@.")

Printer.pp_location print the full path. I want just the line number.

I found pretty_line in Cil_datatype.Location module and tried to use it but I can not. I'm getting compile errors and I have not found an example of using this function in Frama-C sources.

I tried this,

let print_loc kf =             
let locals = Kernel_function.get_locals kf in 
List.iter (fun vi -> 
let line =  Cil_datatype.Location.pretty_line Format.sprintf "%a" Printer.pp_location vi.vdecl in
Format.printf "Line %d: %a %s@." line Printer.pp_typ vi.vtype vi.vname) locals

And I got this error message

Error: This function has type Format.formatter -> Cil_datatype.Location.t -> unit It is applied to too many arguments; maybe you forgot a `;'.

I tried several combinations, but in any case, either I get the previous error message or I get this message:

Error: This expression has type Format.formatter -> Cil_types.location -> unit but an expression was expected of type unit -> 'a -> string Type Format.formatter is not compatible with type unit

Can I get the information about line number otherwise? Or How can I properly use Cil_datatype.Location.pretty_line ?

Thanks

Solution

  • octachtron's answer summarizes nicely how to use pretty_line with a format string. However, if you want to use the line number as an integer (not necessarily to print it with %d), Cil_datatype.Location.t is a concrete type, more precisely an alias to Cil_types.location, which is itself a pair of Lexing.location. Hence, for retrieving the line where the location starts, you can simply do

    ...
let line = (fst vi.vdecl).Lexing.pos_lnum in 
...