[SOLVED] Frama-C: how to get the start line number and the location of starting character?

Frama-C: how to get the start line number and the location of starting character?

Now I have PdgTypes.Node.stmt, I just can use:

Format.printf "%a"
  Printer.pp_location (Cil_datatype.Stmt.loc PdgTypes.Node.stmt)

to print the result like this:

mkdir.c:500

But I want the result that like this:

mkdir.c:500:23

It means that the output should contain the location of starting character. What should I do?

Thanks in advance for your help!

Solution

A Location in Frama-C (defined in module Cil_datatype, in file src/kernel_services/ast_queries/cil_datatype.ml) is a pair of Positions (defined in the same file), the start and end position of an AST element.

A Position is very similar to an OCaml's Lexing.position. The only difference is that Lexing's position has a string field pos_fname, while Frama-C's position has a Datatype.Filepath (defined by Frama-C) field pos_fpath.

Both Location and Position have functions pretty_debug, which includes the character number. Position also has pp_with_col, which prints the column number but in format %a char %d, which is different from what you want.

In any case, these functions can serve as inspiration to the one you want.

Important note: pos_cnum stands for character offset (from the start of the file) and not column offset, so you need to subtract pos_bol, the offset of the beginning of the current line, to get the actual column number of a character: pos_cnum - pos_bol.

Here's an example of some code that should be close to what you want (you may need an open Cil_types or open Cil_datatypes for these to work):

let (pos_start, _pos_end) = Cil_datatype.Stmt.loc PdgTypes.Node.stmt in
Format.fprintf fmt "%a:%d:%d"
  Datatype.Filepath.pretty pos_start.Filepath.pos_path
  pos_start.Filepath.pos_lnum
  (pos_start.Filepath.pos_cnum - pos_start.Filepath.pos_bol)