package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

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

Pretty-prints the path (absolute)

val pretty_rel : Stdlib.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 : 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 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

On This Page

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