Frama-C:
Plug-ins:
Libraries:

Frama-C API - Fileloc

This module handle locations in a source file. Fileloc.t is a Frama-C datatype, and comes with usual compare, equal, hash and pretty functions.

  • compare first compares the starting position of the location then - if they are equal - compares the ending position.
  • hash only hashes the first position.
  • before 33.0-Arsenic

    This module was Cil_datatype.Location.

type t
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
include Datatype.S_with_collections with type t := t
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val ty : t Type.t
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val unknown : t

Special representation of an unknown location.

  • deprecated Use your plug-in generated location via Self.gen_loc or Self.gen_loc_from instead.
val generated : ?loc:t -> string -> t

Make a new location for a generated input. The generator name is given as a string. If the location is provided, it is copied (except for its origin), else it is unknown.

Pretty printing

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty prints a locaton in a short format file:<line1>-<line2>:<char1>-<char2>, with variants depending on if both positions are in the same file/line/column. Generated locations are printed inside a tag <generated by <generator> from <loc>>

val pretty_long : t Pretty_utils.formatter

Pretty prints a locaton in a long format "file", lines <line1>-<line2>, characters <char1>-<char2>, with variants depending on if both positions are in the same file/line/column. Generated locations are printed as such generated by <generator> from <loc>.

val pretty_long_with_inclusions : t Pretty_utils.formatter

Same as pretty_long but also prints the list of inclusion.

val pretty_debug : t Pretty_utils.formatter

Pretty-prints the ocaml internal representation of a location, for debug purposes.

  • since 22.0-Titanium

Conversion from/to Lexing.position

val of_lexing_pos : Stdlib.Lexing.position -> t

Convert a Lexing.position to a Fileloc.t.

  • since Frama-C+dev
val of_lexing_loc : (Stdlib.Lexing.position * Stdlib.Lexing.position) -> t

Convert a pair of Lexing.position to a Fileloc.t.

val to_lexing_loc : t -> Stdlib.Lexing.position * Stdlib.Lexing.position

Convert a pair of Fileloc.t to a Lexing.position.

Accessors

val start_pos : t -> Filepos.t

Get the starting position of a location

  • since Frama-C+dev.
val end_pos : t -> Filepos.t

Get the ending position of a location

  • since Frama-C+dev.
val line : t -> int

Get the first line of the location.

val path : t -> Filepath.t

Get the file path of the location.

val is_empty : t -> bool

is_empty loc returns true if the first position is empty according to Filepos.is_empty.

Constructors

It is not recommended to manipulate / create locations manually, only the parser should do it. But if really necessary, these functions provides ways to to it.

val make : start_pos:Filepos.t -> end_pos:Filepos.t -> t

Create a location between a starting and ending position.

  • since Frama-C+dev
val positions : t -> Filepos.t * Filepos.t

Convert a location to a pair of positions.

  • since Frama-C+dev
val of_pos : Filepos.t -> t

Create a location from the given position.

  • since Frama-C+dev
val join : t -> t -> t

Create a location from the union of two locations using Fileloc.compare to find the starting and ending positions.

  • since Frama-C+dev
val start_loc : t -> t

start_loc loc returns a new location pointing only to the beginning of loc, i.e. reduced to a single position equal to the start of loc.

  • since Frama-C+dev
val end_loc : t -> t

end_loc loc returns a new location pointing only to the end of loc, i.e. reduced to a single position equal to the end of loc.

  • since Frama-C+dev

Datatype with comparison/hash on original source positions

This module provides an alternative datatype where only original location are considered for compare, equal and hash. See Filepos.origin.Original.