diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-03-24 21:01:42 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-25 15:54:40 +0200 |
commit | 679e49dbdc1448c65122eecd24783eb35376d492 (patch) | |
tree | 5055b0e9039d91b6c8cc42b9f7d121ec7c381542 /checker/analyze.mli | |
parent | 9c7b70032972ed613bcca02cceedcd33c240f7a8 (diff) |
Adding a more efficient representation of OCaml objects in votour.
Diffstat (limited to 'checker/analyze.mli')
-rw-r--r-- | checker/analyze.mli | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/checker/analyze.mli b/checker/analyze.mli new file mode 100644 index 000000000..42efcf01d --- /dev/null +++ b/checker/analyze.mli @@ -0,0 +1,35 @@ +type data = +| Int of int +| Ptr of int +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +val parse_channel : in_channel -> (data * obj array) +val parse_string : string -> (data * obj array) + +(** {6 Functorized version} *) + +module type Input = +sig + type t + val input_byte : t -> int + (** Input a single byte *) + val input_binary_int : t -> int + (** Input a big-endian 31-bits signed integer *) +end +(** Type of inputs *) + +module type S = +sig + type input + val parse : input -> (data * obj array) + (** Return the entry point and the reification of the memory out of a + marshalled structure. *) +end + +module Make (M : Input) : S with type input = M.t +(** Functorized version of the previous code. *) |