Frama_c_kernel.Command
Useful high-level system operations.
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.
pp_from_file fmt file
dumps the content of file
into the fmt
. Exceptions in pp
are re-raised after closing.
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
.
copy source target
copies source file to target file using bincopy
.
Properly close the channel and re-raise exceptions
Properly close the channel and re-raise exceptions
Properly flush and close the channel and re-raise exceptions
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.
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.
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.
val command_async :
?stdout:Stdlib.Buffer.t ->
?stderr:Stdlib.Buffer.t ->
string ->
string array ->
unit ->
process_result
Same arguments as Unix
.create_process.