Frama-C:
Plug-ins:
Libraries:

Frama-C API - Filesystem

File system

val exists : Filepath.t -> bool

Equivalent to Sys.file_exists.

  • since 28.0-Nickel
val is_file : Filepath.t -> bool

is_file f returns true iff f points to a regular file (or a symbolic link pointing to a file). Returns false if any errors happen when stat'ing the file.

  • since 22.0-Titanium
val is_dir : Filepath.t -> bool

Equivalent to Sys.is_directory.

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

Equivalent to Sys.readdir.

  • since 28.0-Nickel
  • deprecated Use iter_dir or fold_dir instead
val list_dir : Filepath.t -> string list

Contents of a directory.

  • since Frama-C+dev
val iter_dir : (string -> unit) -> Filepath.t -> unit

Iter through the contents of a directory.

  • since Frama-C+dev
val fold_dir : (string -> 'a -> 'a) -> Filepath.t -> 'a -> 'a

Fold over the contents of a directory.

  • since Frama-C+dev
val make_dir : ?parents:bool -> Filepath.t -> Unix.file_perm -> bool

make_dir ?parents name perm creates directory name with permission perm. If parents is true, recursively create parent directories if needed. parents defaults to false. Note that this function may create some of the parent directories and then fail to create the children, e.g. if perm does not allow user execution of the created directory. This will leave the filesystem in a modified state before raising an exception. Returns true if the directory was created, false otherwise.

  • raises Unix.Unix_error

    if cannot create name or its parents.

  • raises Failure

    if the path exists but is not a directory

  • since 19.0-Potassium
  • before 28.0-Nickel

    name argument was of type string and the returned type was unit. Also, the function did not check for path's existence.

val remove_file : Filepath.t -> unit

Tries to delete a file and never fails.

  • before Frama-C+dev

    it was Extlib.safe_remove

val remove_dir : Filepath.t -> unit

Tries to delete a directory and never fails.

  • before Frama-C+dev

    it was Extlib.safe_remove_dir

val rename : Filepath.t -> Filepath.t -> unit

Equivalent to Sys.rename.

  • since 28.0-Nickel

Temporary files

See Temp_files module for automatic removal of temp files at exit.

exception Temp_file_error of string
val temp_file : prefix:string -> suffix:string -> Filepath.t

Similar to Filename.temp_file.

  • since Frama-C+dev
val temp_dir : prefix:string -> suffix:string -> Filepath.t

Similar to Filename.temp_dir.

  • since Frama-C+dev

File comparison

val digest : Filepath.t -> string

digest p computes the hash of a file p using Stdlib.Digest.file.

  • since Frama-C+dev
val same_digest : Filepath.t -> Filepath.t -> bool

same_digest p1 p2 compares the hashes of two files p1 and p2 using Stdlib.Digest.file and returns true if they have the same.

  • since Frama-C+dev

High level Input/Output

val bincopy : bytes -> Stdlib.in_channel -> Stdlib.out_channel -> unit
  • deprecated This function is only used locally and is not exported anymore.
val copy_file : Filepath.t -> Filepath.t -> unit

copy_file source target copies source file to target file.

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

    this function was Command.copy

val iter_lines : Filepath.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

Low level file Input/Output

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 -> Filepath.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 -> Filepath.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 -> Filepath.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 -> Filepath.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 : Filepath.t -> (Stdlib.Format.formatter, 'a) safe_processor

with_formatter 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 : Filepath.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 Compressed : sig ... end
module Operators : sig ... end

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