Command (p.frama-c.28.0.doc.frama-c.kernel.Frama_c

File Utilities

val pp_to_file : Filepath.Normalized.t -> (Format.formatter -> unit) -> unit

pp_to_file file pp runs pp on a formatter that writes into file. The formatter is always properly flushed and closed on return. Exceptions in pp are re-raised after closing.

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

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

val bincopy : bytes -> in_channel -> out_channel -> unit

copy buffer cin cout reads cin until end-of-file and copy it in cout. buffer is a temporary string used during the copy. Recommended size is 2048.

val copy : Filepath.Normalized.t -> Filepath.Normalized.t -> unit

copy source target copies source file to target file using bincopy.

val read_file : Filepath.Normalized.t -> (in_channel -> 'a) -> 'a

Properly close the channel and re-raise exceptions

val read_lines : Filepath.Normalized.t -> (string -> unit) -> unit

Iter over all text lines in the file

val write_file : Filepath.Normalized.t -> (out_channel -> 'a) -> 'a

Properly close the channel and re-raise exceptions

val print_file : Filepath.Normalized.t -> (Format.formatter -> 'a) -> 'a

Properly flush and close the channel and re-raise exceptions

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

Same arguments as Unix.create_process but returns only when execution is complete.

raises Sys_error
when a system error occurs

type process_result =

| Not_ready of unit -> unit
| 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

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.

raises Sys_error
when a system error occurs

val command_async : 
  ?stdout:Buffer.t ->
  ?stderr:Buffer.t ->
  string ->
  string array ->
  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.

raises Sys_error
when a system error occurs

val command : 
  ?timeout:int ->
  ?stdout:Buffer.t ->
  ?stderr:Buffer.t ->
  string ->
  string array ->
  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 Sys_error
when a system error occurs

raises Db.Cancel
when the computation is interrupted or on timeout