aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/analyze.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-28 12:51:24 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-28 13:34:47 +0100
commit8f47273f118808373649a3a084e4a3c99167edd3 (patch)
tree3a316928b3605cc9f87d6b630a45ccbe9b492152 /checker/analyze.mli
parentd8093626b49b539bec283285ea37ba50e79f69d4 (diff)
Use safe demarshalling in the checker.
Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations.
Diffstat (limited to 'checker/analyze.mli')
-rw-r--r--checker/analyze.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/analyze.mli b/checker/analyze.mli
index 1b6c94759..9c837643f 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -45,3 +45,6 @@ end
module Make (M : Input) : S with type input = M.t
(** Functorized version of the previous code. *)
+
+val instantiate : data * obj LargeArray.t -> Obj.t
+(** Create the OCaml object out of the reified representation. *)