aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/analyze.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-03-24 21:01:42 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-25 15:54:40 +0200
commit679e49dbdc1448c65122eecd24783eb35376d492 (patch)
tree5055b0e9039d91b6c8cc42b9f7d121ec7c381542 /checker/analyze.mli
parent9c7b70032972ed613bcca02cceedcd33c240f7a8 (diff)
Adding a more efficient representation of OCaml objects in votour.
Diffstat (limited to 'checker/analyze.mli')
-rw-r--r--checker/analyze.mli35
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. *)