Frama-C:
Plug-ins:
Libraries:

Frama-C API - Filepath

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

type t

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 is 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 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 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 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 pretty_abs : Stdlib.Format.formatter -> t -> unit

Pretty-prints as absolute path, without symbolic names.

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

Pretty-prints as relative path relative to current working directory, without symbolic names.

val dummy : t

Dummy filepath.

  • since Frama-C+dec

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 31.0-Gallium

    this function was normalize

val to_string : t -> string

to_string p returns p prettified, that is, a relative path-like string. The resulting string may contain symbolic dirs, thus it is not a path.

val to_string_rel : ?quoted:bool -> ?base:t -> t -> string

to_string_rel ?quoted ?base p returns p relativized, if relative to base, or its absolute path otherwise. The resulting string has no symbolic names, thus it can be converted back to Filepath.t.

  • parameter ?quoted

    if set the string will be suitable for use as one argument in a command line, defaults to false.

  • parameter ?base

    the base directory to be relative to, defaults to current working directory.

  • since Aluminium-20160501
  • before 31.0-Gallium

    was named relativize, argument types were string instead of t and the named argument was base_name

val to_string_abs : ?quoted:bool -> t -> string

to_string_abs p returns p absolutized. The resulting string has no symbolic names, thus it can be converted back to Filepath.t.

  • parameter ?quoted

    if set the string will be suitable for use as one argument in a command line, defaults to false

  • since 31.0-Gallium
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 -> Hpath.base * string

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

  • if it starts with symbolic path SYMB, prefix is Hpath.Name "SYMB";
  • if it is a relative path, prefix is Hpath.Cwd;
  • else (an absolute path), prefix is Hpath.Absolute. rest contains everything after the '/' following the prefix. E.g. for the path "FRAMAC_SHARE/libc/string.h", returns (Name "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 extension : t -> string

Equivalent to Filename.extension.

  • since 32.0-Germanium
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 31.0-Gallium

    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.(dir / file) is equivalent to Filepath.concat dir file.

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 31.0-Gallium
val chop_suffix : t -> string -> t

Same as Filename.chop_suffix.

  • raises Invalid_argument

    if the suffix does not appear in the filepath.

  • since 31.0-Gallium
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 31.0-Gallium

    named argument was base_name

val sanitize_filename : string -> string

sanitize_filename name returns the given filename with every character not allowed as filename replaced with _. Note that this function takes a file name so path separators like / and \ are replaced.

  • since 32.0-Germanium

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 31.0-Gallium
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