package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Basic datatype functions
Constant paths
Path manipulation
Current working directory
Symboling Names
Position in source file
Deprecated functions

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Filepath/index.html

Module `Frama_c_kernel.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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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

Pretty-prints the path (absolute)

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

Pretty-prints the path (relative to current working dir)

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 =

| Must_exist
(*
File must exist.
*)
| Must_not_exist
(*
File must not exist.
*)
| 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. Note that this prettified string may contain symbolic dirs and is thus is not a path.

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

to_string_rel ?quoted p returns p relativized if it is relative, or returns the absolute path otherwise.

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 cwd

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_rel p returns p absolutized.

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 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.(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 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

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 = {

pos_path : t;
pos_lnum : int;
pos_bol : int;
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 : 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 relativize : ?base:t -> t -> string

deprecated Use Filepath.to_string_rel 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