diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /kernel/cemitcodes.ml | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r-- | kernel/cemitcodes.ml | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 71a9aa0e..4e09a0ed 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -23,7 +23,7 @@ let patch_int buff pos n = let out_buffer = ref(String.create 1024) and out_position = ref 0 - +(* let out_word b1 b2 b3 b4 = let p = !out_position in if p >= String.length !out_buffer then begin @@ -37,6 +37,28 @@ let out_word b1 b2 b3 b4 = String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); out_position := p + 4 +*) +let out_word b1 b2 b3 b4 = + let p = !out_position in + if p >= String.length !out_buffer then begin + let len = String.length !out_buffer in + let new_len = + if len <= Sys.max_string_length / 2 + then 2 * len + else + if len = Sys.max_string_length + then raise (Invalid_argument "String.create") (* Pas la bonne execption +.... *) + else Sys.max_string_length in + let new_buffer = String.create new_len in + String.blit !out_buffer 0 new_buffer 0 len; + out_buffer := new_buffer + end; + String.unsafe_set !out_buffer p (Char.unsafe_chr b1); + String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); + String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); + String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); + out_position := p + 4 let out opcode = out_word opcode 0 0 0 |