Module Journal

module Journal: sig .. end
Journalization of functions.
Consult the Plugin Development Guide for additional details.


Journalization


val register : string ->
'a Type.t -> ?comment:(Format.formatter -> unit) -> ?is_dyn:bool -> 'a -> 'a
register name ty ~comment ~is_dyn v journalizes the value v of type ty with the name name. name must exactly match the caml long name of the value (i.e. "List.iter" and not "iter" even though the module List is already opened). Journalisation of anonymous value is not possible.

If the comment argument is set, the given pretty printer will be applied in an OCaml comment when the function is journalized.

Set is_dyn to true to journalize a dynamic function.

val never_write : string -> 'a -> 'a
never_write name f returns a closure g observationally equal to f except that trying to write a call to g in the journal is an error. If f is not a closure, then never_write name f raises Invalid_argument.
val prevent : ('a -> 'b) -> 'a -> 'b
prevent f x applies x to f without printing anything in the journal, even if f is journalized.
module Binding: sig .. end
module Reverse_binding: sig .. end

Journal management


val get_name : unit -> string
Returns the filename which the journal will be written into.
val set_name : string -> unit
set_name name changes the filename into the journal is generated.
val write : unit -> unit
write () writes the content of the journal into the file set by set_name (or in "frama_c_journal.ml" by default); without clearing the journal.
val save : unit -> unit
Save the current state of the journal for future restoration.
Since Beryllium-20090901
val restore : unit -> unit
Restore a previously saved journal.
Since Beryllium-20090901

Internal use only


val keep_file : string -> unit
This function has not to be used explicitly. Only offers functions retrieving when running a journal file.
val get_session_file : (string -> string) Pervasives.ref