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] How can I get line number from Cil_types.location

Hello,

The function pretty_line is indeed the right function to /print/ the 
line number of a location.

The Cil_datatype.Location.t type is a pair of Lexing.position, as in 
(start, end), although in practice the end position is rarely (if ever) 
used. So if you have just a Lexing.position and want to use that 
pretty-printing function, you can just create a pair by doubling it, 
e.g.: (loc, loc), and it should work in most cases.

However, from your example code, it seems like you want to /get/ the 
line number in OCaml, not print it. In that case, the line number is 
just the pos_lnum field of the record Lexing.position, so you can do:

let line = (fst loc).Lexing.pos_lnum in
...

This is exactly what is done in 
src/kernel_services/ast_queries/cil_datatype.ml, so you can look in that 
code for some inspiration.

Overall, Frama-C uses Lexing.position for source code locations, so you 
can take a look at OCaml's Lexing module for more details.


On 11/03/18 21:39, Rokiatou DIARRA wrote:
> Hi,
>
> I want to get only line number in source file. With 
> Printer.pp_location I get the full path to the source like 
> <dir/f>:<l>. But I want just the line number.
>
> I looked in Frama-c sources, and I found in Cil_datatype.Location 
> module a printer : *val pretty_line: t Pretty_utils.formatter *.
>
> So I tried it with the following instructions:
>
>     let line =( Cil_datatype.Location.pretty_line loc); (where loc has 
> type Cil_types.location = Lexing.position * Lexing.position) but I got 
> this error message:
>
> Error: This expression has type
>          Cil_types.location = Lexing.position * Lexing.position
>        but an expression was expected of type Lexing.position
>
> Are there any functions, in Frama-C, to get only the line number?
>
> Thanks.
>
> Rokiatou DIARRA
> E-Mail: diarr_rokiatou at yahoo.fr
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Researcher/Engineer CEA/LIST
Software Reliability and Security Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180313/0c27010d/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180313/0c27010d/attachment-0001.bin>