Frama-C:
Plug-ins:
Libraries:

Frama-C API - Filepath

Functions manipulating normalized filepaths. In these functions, references *he current working directory refer to the result given by function Sys.getcwd.

type t = private string

A normalized (absolute) path.

Basic datatype functions

Filepath.t is a Frama-C datatype, and comes with usual compare, equal, hash and pretty functions.

Pretty-print is done according to these rules:

  • relative filenames are kept, except for leading './', which are stripped;
  • absolute filenames are relativized if their prefix is included in the current working directory; also, symbolic names are resolved, i.e. the result may be prefixed by known aliases (e.g. FRAMAC_SHARE). See add_symbolic_dir for more details. Therefore, the result of this function may not designate a valid name in the filesystem and must ONLY be used to pretty-print information; it must NEVER to be converted back to a filepath later on.
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 name : string

Unique name of the datatype.

val 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 pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

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 compare_pretty : ?case_sensitive:bool -> t -> t -> int

Compares prettified (i.e. relative) paths, with or without case sensitivity (by default, case_sensitive = false).

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

Pretty-prints the normalized (absolute) path.

Constant paths

val empty : t

Empty filepath.

  • since 23.0-Vanadium.
val is_empty : t -> bool
  • since 23.0-Vanadium
val is_special_stdout : t -> bool

is_special_stdout f returns true iff f is '-' (a single dash), which is a special notation for 'stdout'.

  • since 23.0-Vanadium

Path manipulation

type existence =
  1. | Must_exist
    (*

    File must exist.

    *)
  2. | Must_not_exist
    (*

    File must not exist.

    *)
  3. | Indifferent
    (*

    No requirement.

    *)

Existence requirement on a file.

exception No_file

Raised whenever no file exists and existence is Must_exist.

exception File_exists

Raised whenever some file exists and existence is Must_not_exist.

val of_string : ?existence:existence -> ?base:t -> string -> t

Returns an absolute path leading to the given file. The result is similar to realpath --no-symlinks. Some special behaviors include:

  • normalize "" (empty string) returns "" (realpath returns an error);
  • normalize preserves multiple sequential '/' characters, unlike realpath;
  • non-existing directories in realpath may lead to ENOTDIR errors, but normalize may accept them.
  • before 21.0-Scandium

    no existence argument.

  • before Frama-C+dev

    this function was normalize

val to_pretty_string : t -> string

to_pretty_string p returns p prettified, that is, a relative path-like string. Note that this prettified string may contain symbolic dirs and is thus is not a path. See pretty for details about usage.

val to_pretty_relative : ?base:t -> t -> string

to_pretty_relative p returns p relativized if it is relative, or returns the same thing as to_pretty_string otherwise.

  • since Frama-C+dev
val to_quoted_string : t -> string

to_quoted_string p returns p but quoted, suitable for use as one argument in a command line. See Filename.quoted

  • since Frama-C+dev
val to_string_list : t list -> string list

to_string_list l returns l as a list of strings containing the absolute paths to the elements of l.

  • since 23.0-Vanadium
val to_base_uri : t -> string option * string

to_base_uri path returns a pair prefix, rest, according to the prettified value of path:

  • if it starts with symbolic path SYMB, prefix is Some "SYMB";
  • if it is a relative path, prefix is Some "PWD";
  • else (an absolute path), prefix is None. rest contains everything after the '/' following the prefix. E.g. for the path "FRAMAC_SHARE/libc/string.h", returns ("FRAMAC_SHARE", "libc/string.h").
  • since 22.0-Titanium
val basename : t -> string

Equivalent to Filename.basename.

  • since 28.0-Nickel
val dirname : t -> t

Equivalent to Filename.dirname.

  • since 28.0-Nickel
val extend : ?existence:existence -> t -> string -> t

extend ~existence file ext returns the normalized path to the file file ^ ext. Note that it does not introduce a dot. The resulting path must respect existence.

  • since 29.0-Copper
  • before Frama-C+dev

    this function was Normalize.extend

val concat : ?existence:existence -> t -> string -> t

concat ~existence dir file returns the normalized path resulting from the concatenation of dir ^ "/" ^ file. The resulting path must respect existence.

  • since 22.0-Titanium
val (/) : t -> string -> t

Operator version of Filepath.concat. Filepath.(file / ext) is equivalent to Filepath.concat file ext.

val concats : ?existence:existence -> t -> string list -> t

concats ~existence dir paths concatenates a list of paths, as per the concat function.

  • since 28.0-Nickel
val has_suffix : t -> string -> bool

Same as Filename.check_suffix.

  • since Frama-C+dev
val chop_suffix : t -> string -> t

Same as Filename.chop_suffix.

  • raises Invalid_argument

    if the suffix does not appear in the filepath.

  • since Frama-C+dev
val is_relative : ?base:t -> t -> bool
  • returns

    true if the file is relative to base (that is, it is prefixed by base), or to the current working directory if no base is specified.

  • since Aluminium-20160501
  • before 23.0-Vanadium

    argument types were string instead of t.

  • before Frama-C+dev

    named argument was base_name

val relativize : ?base:t -> t -> string

relativize base file_name returns a relative path name of file_name w.r.t. base, if base is a prefix of file; otherwise, returns file_name unchanged. The default base name is the current working directory name.

  • since Aluminium-20160501
  • before Frama-C+dev

    argument types were string instead of t and named argument was base_name

Current working directory

val pwd : unit -> t
  • returns

    the current working directory. Implicitly uses Unix.realpath to normalize paths and avoid issues with symbolic links in directory names.

  • since 25.0-Manganese
  • before 28.0-Nickel

    return type was string instead of t.

Symboling Names

val add_symbolic_dir : string -> t -> unit

add_symbolic_dir name dir indicates that the (absolute) path dir must be replaced by name when pretty-printing paths. This alias ensures that system-dependent paths such as FRAMAC_SHARE are printed identically in different machines.

val add_symbolic_dir_list : string -> t list -> unit
val remove_symbolic_dir : t -> unit

Remove all symbolic dirs that have been added earlier.

  • since Frama-C+dev
val reset_symbolic_dirs : unit -> unit

Remove all symbolic dirs that have been added earlier.

  • since 23.0-Vanadium
val all_symbolic_dirs : unit -> (string * t) list

Returns the list of symbolic dirs added via add_symbolic_dir, plus preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir).

  • since 22.0-Titanium

Position in source file

type position = {
  1. pos_path : t;
  2. pos_lnum : int;
  3. pos_bol : int;
  4. pos_cnum : int;
}

Describes a position in a source file.

  • since 18.0-Argon
val empty_pos : position

Empty position, used as 'dummy' for Cil_datatype.Position.

  • since 30.0-Zinc
val pp_pos : Stdlib.Format.formatter -> position -> unit

Pretty-prints a position, in the format file:line.

  • since 18.0-Argon
val is_empty_pos : position -> bool

Return true if the given position is the empty position.

  • since 30.0-Zinc

Deprecated functions

val normalize : ?existence:existence -> ?base_name:string -> string -> string
  • deprecated Use Filepath.of_string instead.
val exists : t -> bool
  • deprecated Use Filesystem.exists instead
val is_file : t -> bool
  • deprecated Use Filesystem.is_file instead
val is_dir : t -> bool
  • deprecated Use Filesystem.is_dir instead
val readdir : t -> string array
  • deprecated Use Filesystem.readdir instead
val remove : t -> unit
  • deprecated Use Filesystem.remove_file instead
val rename : t -> t -> unit
  • deprecated Use Filesystem.rename instead
val copy_file : t -> t -> unit
  • deprecated Use Filesystem.copy_file instead
val iter_lines : t -> (string -> unit) -> unit
  • deprecated Use Filesystem.iter_lines instead
module Normalized : sig ... end