diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-23 15:05:50 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-14 16:16:57 +0100 |
commit | 96a4c2a8e2b3de327331e55a9663d230027210e9 (patch) | |
tree | 5f55206aa91300c5673ecba8b2e6098072fb4660 /kernel | |
parent | 8fa3c26adb1bc2c0201a61adede278a0e889eef4 (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.ml | 17 |
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 *) |