aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
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 /kernel
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.
Diffstat (limited to 'kernel')
-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 *)