Frama-C:
Plug-ins:
Libraries:

Frama-C API - Filepath

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

NOTE: Prefer using the Normalized module whenever possible.

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 normalize : ?existence:existence -> ?base_name:string -> string -> string

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.

val relativize : ?base_name:string -> string -> string

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

  • since Aluminium-20160501
module Normalized : sig ... end

The Normalized module is simply a wrapper that ensures that paths are always normalized. Used by Datatype.Filepath.

val is_relative : ?base_name:Normalized.t -> Normalized.t -> bool

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

  • since Aluminium-20160501
  • before 23.0-Vanadium

    argument types were string instead of Normalized.t.

val add_symbolic_dir : string -> Normalized.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 -> Normalized.t list -> unit
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 * Normalized.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
type position = {
  1. pos_path : Normalized.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
val pwd : unit -> Normalized.t

Return 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 Normalized.t.

val exists : Normalized.t -> bool

Equivalent to Sys.file_exists.

  • since 28.0-Nickel
val is_dir : Normalized.t -> bool

Equivalent to Sys.is_directory.

  • since 28.0-Nickel
val readdir : Normalized.t -> string array

Equivalent to Sys.readdir.

  • since 28.0-Nickel
val remove : Normalized.t -> unit

Equivalent to Sys.remove.

  • since 28.0-Nickel
val rename : Normalized.t -> Normalized.t -> unit

Equivalent to Sys.rename.

  • since 28.0-Nickel
val basename : Normalized.t -> string

Equivalent to Filename.basename.

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

Equivalent to Filename.dirname.

  • since 28.0-Nickel
val bincopy : bytes -> Stdlib.in_channel -> Stdlib.out_channel -> unit
  • deprecated This function is only used locally and is not exported anymore.
val copy : Normalized.t -> Normalized.t -> unit

copy source target copies source file to target file.

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

    this function was Command.copy

val iter_lines : Normalized.t -> (string -> unit) -> unit

Iter over all text lines in the file

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

    this function was Command.read_lines

type action_if_missing =
  1. | Create of int
    (*

    create the file with the given permissions

    *)
  2. | DoNotCreate
    (*

    do not create the file and fail

    *)

This type defines what action with_open_in and with_open_out must perform when the file to open does not exist.

type action_if_exists =
  1. | Error
    (*

    file opening functions will fail with an error

    *)
  2. | Append
    (*

    the writing contents will be appended

    *)
  3. | Truncate
    (*

    the file will be truncated before any writes

    *)

This type define what action with_open_out must perform when the file to open already exists.

type ('ch, 'a) safe_processor = ('ch -> 'a) -> ('a, string) Stdlib.result

A safe_processor helps to handle file operations while ensuring the file will be closed no matter what happens. It is a function that takes a file operation f as a parameter, opens a file and calls the f with the newly-created channel.

type ('ch, 'a) exn_processor = ('ch -> 'a) -> 'a

Same as safe_processor but when a Sys_error is raised, re-raise it after closing the file

val with_open_in : ?if_missing:action_if_missing -> ?binary:bool -> ?blocking:bool -> Normalized.t -> (Stdlib.in_channel, 'a) safe_processor

with_open_in path f opens file path for reading and calls f with the newly-created input channel. The file is closed when f returns or whenever an exception is thrown by f.

  • parameter if_missing

    defines what must be done if the file does not exist, defaults to DoNotCreate.

  • parameter binary

    must be set if the file needs to be opened in binary mode (disables conversion, e.g. new lines), defaults to false

  • parameter blocking

    must be unset if the file needs to be opened in nonblocking mode, defaults to true.

  • returns

    Ok (f input_channel) if no exceptions are thrown, or Error s if a Sys_error s is thrown during the execution of f or during the closing of the file.

  • since Frama-C+dev
val with_open_in_exn : ?if_missing:action_if_missing -> ?binary:bool -> ?blocking:bool -> Normalized.t -> (Stdlib.in_channel, 'a) exn_processor

Same as with_open_in but raises Sys_error instead of returning Error.

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

    this function was Command.read_file

val with_open_out : ?if_missing:action_if_missing -> ?if_exists:action_if_exists -> ?binary:bool -> ?blocking:bool -> Normalized.t -> (Stdlib.out_channel, 'a) safe_processor

with_open_out path f calls f with a new output channel on the file path opened for writing. The file is closed when f returns or whenever an exception is thrown by f.

  • parameter if_missing

    defines what must be done if the file does not exist, defaults to Create 0o666.

  • parameter if_exists

    defines what action must be performed when the file already exists, defaults to Truncate.

  • parameter binary

    must be set if the file needs to be opened in binary mode (disables conversion, e.g. new lines), defaults to false.

  • parameter blocking

    must be unset if the file needs to be opened in nonblocking mode, defaults to true.

  • returns

    Ok (f output_channel) if no exceptions are thrown, or Error s if a Sys_error s is thrown during the execution of f or during the closing the file.

  • since Frama-C+dev
val with_open_out_exn : ?if_missing:action_if_missing -> ?if_exists:action_if_exists -> ?binary:bool -> ?blocking:bool -> Normalized.t -> (Stdlib.out_channel, 'a) exn_processor

Same as with_open_out but raises Sys_error instead of returning Error.

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

    this function was Command.write_file

val with_formatter : Normalized.t -> (Stdlib.Format.formatter, 'a) safe_processor

with_formatter_exn path f calls f with a formatter writing to the file path. The file is closed and the formatter is flushed when f returns or whenever an exception is thrown by f.

  • returns

    Ok (f fmt) if no exceptions are thrown, or Error s if a Sys_error s is thrown during the execution of f or when closing the file.

  • since Frama-C+dev
val with_formatter_exn : Normalized.t -> (Stdlib.Format.formatter, 'a) exn_processor

Same as with_formatter but raises Sys_error instead of returning Error.

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

    this function was Command.pp_to_file and Command.print_file

module Operators : sig ... end

Opening this module allows to use shorter syntax to deal with files.