Module Frama_c_kernel.Command

Useful high-level system operations.

File Utilities

val pp_to_file : Filepath.t -> (Format.formatter -> unit) -> unit
  • deprecated Use Filesystem.with_formatter_exn instead.
val bincopy : bytes -> in_channel -> out_channel -> unit
  • deprecated This function is only used locally and is not exported anymore.
val copy : Filepath.t -> Filepath.t -> unit
  • deprecated Use Filesystem.copy instead.
val read_file : Filepath.t -> (in_channel -> 'a) -> 'a
  • deprecated Use Filesystem.with_open_in_exn instead.
val read_lines : Filepath.t -> (string -> unit) -> unit
  • deprecated Use Filesystem.iter_lines instead.
val write_file : Filepath.t -> (out_channel -> 'a) -> 'a
  • deprecated Use Filesystem.with_open_out_exn instead.
val print_file : Filepath.t -> (Format.formatter -> 'a) -> 'a
  • deprecated Use Filesystem.with_formatter_exn instead.

Pretty from files

val pp_from_file : Format.formatter -> Filepath.t -> unit

pp_from_file fmt file dumps the content of file into the fmt. Exceptions in pp are re-raised after closing.

Timing Utility

type timer = float ref
val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b

Compute the elapsed time with Sys.time. The rmax timer is maximized and the radd timer is cumulated. Computed result is returned, or exception is re-raised.

System commands

val full_command : string -> string array -> stdin:Unix.file_descr -> stdout:Unix.file_descr -> stderr:Unix.file_descr -> Unix.process_status
  • deprecated This unused function was removed from Frama-C.
type process_result =
  1. | Not_ready of unit -> unit
  2. | Result of Unix.process_status
    (*

    Not_ready f means that the child process is not yet finished and may be terminated manually with f ().

    *)
val full_command_async : string -> string array -> stdin:Unix.file_descr -> stdout:Unix.file_descr -> stderr:Unix.file_descr -> unit -> process_result
  • deprecated This unused function was removed from Frama-C.
val async : ?stdout:Buffer.t -> ?stderr:Buffer.t -> string -> string list -> unit -> process_result

Same arguments as Unix.create_process.

  • returns

    a function to call to check if the process execution is complete. You must call this function until it returns a Result to prevent Zombie processes. When this function returns a Result, the stdout and stderr of the child process will be filled into the arguments buffer.

  • before 31.0-Gallium

    this function was named command_async

val command_async : ?stdout:Buffer.t -> ?stderr:Buffer.t -> string -> string list -> unit -> process_result
  • deprecated Use Command.async instead.
val spawn : ?timeout:int -> ?stdout:Buffer.t -> ?stderr:Buffer.t -> string -> string list -> Unix.process_status

Same arguments as Unix.create_process. When this function returns, the stdout and stderr of the child process will be filled into the arguments buffer.

  • raises Async.Cancel

    when the computation is interrupted or on timeout

  • before 29.0-Copper

    Async.Cancel was Db.Cancel

  • before 31.0-Gallium

    this function was named command

val command : ?timeout:int -> ?stdout:Buffer.t -> ?stderr:Buffer.t -> string -> string list -> Unix.process_status
  • deprecated Use Command.spawn instead.