Frama-C API - `Filesystem`

The set of functions in Filesystem are provided both as a convenient way to use Filepath.t directly (without conversion) and to be safer variants than the standard library's or Unix library's.

They are safer in several ways:

some of them are intended to never fail (dir_exists, remove_file, etc.);
some of them return a Result.t (file_kind, with_open_in, etc.) which forces the caller to be careful about the possible errors;
the others will uniformly raise Sys_error - possibly converted from Unix.Unix_error - so the handling of exceptions is a bit lighter;
all the functions taking a file path as argument will check that the path is not empty and may raise Invalid_argument if it is not the case.

The module documentation should mention all the possible exceptions raised and the caller should always catch Sys_error if needed. Empty file paths are considered a programming error, and the emptiness should be checked by the caller beforehand. Thus, the caller should not catch Invalid_argument.

Error handling

type error = string * Filepath.t

type nonrec 'a result = ('a, error) Stdlib.result

File system

type file_kind =

| File
| Directory
| CharacterDevice
| BlockDevice
| SymbolicLink
| NamedPipe
| Socket

This type is used to determine the type of file a path refers to.

since Frama-C+dev

val file_kind : Filepath.t -> file_kind result

file_kind p returns the file kind of the given path p. On failure - for instance if the file does not exist - returns an error string.

raises Invalid_argument
if p is empty

since Frama-C+dev

val exists : Filepath.t -> bool

exists p returns whether the path p points to an existing file (of any kind) p. Equivalent to Sys.file_exists.

raises Invalid_argument
if the path is empty

since 28.0-Nickel

val file_exists : Filepath.t -> bool

file_exists p returns whether the path points to an existing regular file. It is equivalent to file_kind p = Ok (File)

raises Invalid_argument
if p is empty

since Frama-C+dev

val dir_exists : Filepath.t -> bool

dir_exists p returns whether the path points to an existing directory, It is equivalent to file_kind p = Ok (Directory)

raises Invalid_argument
if p is empty

since Frama-C+dev

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

deprecated use file_exists instead.

val is_dir : Filepath.t -> bool

Equivalent to Sys.is_directory.

since 28.0-Nickel

deprecated use dir_exists instead.

val list_dir : Filepath.t -> string list

Contents of a directory.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

val iter_dir : (string -> unit) -> Filepath.t -> unit

Iter through the contents of a directory.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

val fold_dir : (string -> 'a -> 'a) -> Filepath.t -> 'a -> 'a

Fold over the contents of a directory.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

val make_dir : ?parents:bool -> ?perm:int -> Filepath.t -> unit

make_dir ?parents ?perm filepath creates directory filepath with permission perm (default is 0o755). If the directory already exists, this function does nothing. However, if the path points to an existing file that is not a directory, the function raises Sys_error. If parents is true (the default), recursively create parent directories if needed. 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 Sys_error.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 19.0-Potassium

before 28.0-Nickel
name argument was of type string. Also, the function did not check for path's existence.

before Frama-C+dev
the function raised Invalid_argument instead of Sys_error when the path pointed to an existing file that was not a directory. Also the perm argument was not named and the return type was bool to indicate whether the directory has actually been created or if it already existed.

val remove_file : Filepath.t -> unit

Tries to delete a file and never fails.

before 31.0-Gallium
it was Extlib.safe_remove

val remove_dir : Filepath.t -> unit

Tries to delete a directory and never fails.

before 31.0-Gallium
it was Extlib.safe_remove_dir

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

rename source target rename the file source to target. Equivalent to Sys.rename.

raises Sys_error
if a system error occurred

raises Invalid_argument
if one of the paths is empty

since 28.0-Nickel

Temporary files

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

val temp_file : prefix:string -> suffix:string -> Filepath.t

Similar to Filename.temp_file.

raises Sys_error
if the temp file cannot be created.

since 31.0-Gallium

before Frama-C+dev
raised a removed Temp_file exception

val temp_dir : prefix:string -> suffix:string -> Filepath.t

Similar to Filename.temp_dir.

raises Sys_error
if the temp dir cannot be created.

since 31.0-Gallium

before Frama-C+dev
raised a removed Temp_file exception

File comparison

val digest : Filepath.t -> string

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

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

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.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

High level Input/Output

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

copy_file source target copies source file to target file.

raises Sys_error
if a system error occurred

raises Invalid_argument
if one of the paths is empty

since 31.0-Gallium

before 31.0-Gallium
this function was Command.copy

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

Iter over all text lines in the file

raises Sys_error
if a system error occurred

raises Invalid_argument
if one of the paths is empty

since 31.0-Gallium

before 31.0-Gallium
this function was Command.read_lines

Low level file Input/Output

type action_if_missing =

| Create of int
(*
create the file with the given permissions
*)
| 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 =

| Error
(*
file opening functions will fail with an error
*)
| Append
(*
the writing contents will be appended
*)
| 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 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 a Sys_error 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.

raises Invalid_argument
if the path is empty

returns
Ok (f input_channel) if no Sys_errors 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 31.0-Gallium

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

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

before 31.0-Gallium
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 a Sys_error 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.

raises Invalid_argument
if the path is empty

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

since 31.0-Gallium

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

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

before 31.0-Gallium
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 a Sys_error is thrown by f.

raises Invalid_argument
if the path is empty

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

since 31.0-Gallium

val with_formatter_exn : Filepath.t -> (Stdlib.Format.formatter, 'a) exn_processor

Same as with_formatter but raises Sys_error instead of returning Error.

raises Sys_error
if a system error occurred

raises Invalid_argument
if the path is empty

since 31.0-Gallium

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