aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-23 15:05:50 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-14 16:16:57 +0100
commit96a4c2a8e2b3de327331e55a9663d230027210e9 (patch)
tree5f55206aa91300c5673ecba8b2e6098072fb4660
parent8fa3c26adb1bc2c0201a61adede278a0e889eef4 (diff)
Remove the unsafe bytes conversion function in Cemitcodes.
This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way.
-rw-r--r--kernel/cemitcodes.ml17
1 files changed, 3 insertions, 14 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 41494441b..f6b9f34ee 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -17,7 +17,7 @@ open Mod_subst
type emitcodes = String.t
-external tcode_of_code : emitcodes -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
(* Relocation information *)
type reloc_info =
@@ -46,25 +46,14 @@ let patch_int buff patches =
and results in wrong results. Side-effects... *)
let buff = Bytes.of_string buff in
let () = List.iter (fun p -> patch buff p) patches in
- (* Note: we follow the apporach suggested by Gabriel Scherer in
- PR#136 here, and use unsafe as we own buff.
-
- The crux of the question that avoids defining emitcodes just as a
- Byte.t is the call to hcons in to_memory below. Even if disabling
- this optimization has no visible time impact, test data shows
- that the optimization is indeed triggered quite often so we
- choose ugliness over altering the semantics.
-
- Handle with care.
- *)
- Bytes.unsafe_to_string buff
+ buff
let patch buff pl f =
let map (r, pos) = (pos, f r) in
(** Order seems important here? *)
let patches = CList.map_left map pl in
let buff = patch_int buff patches in
- tcode_of_code buff (String.length buff)
+ tcode_of_code buff (Bytes.length buff)
(* Buffering of bytecode *)