Reputation: 1373
I am doing the convert type in Ocaml from int
into int32
. I changed some functions of String
Ocaml's library (code below)
external length : string -> int32 = "%string_length"
external create: int32 -> string = "caml_create_string"
external unsafe_blit : string -> int32 -> string -> int32 -> int32 -> unit
= "caml_blit_string" "noalloc"
let sub s ofs len =
if ofs < 0l or len < 0l or add ofs len > length s
then invalid_arg "String.sub"
else begin
let r = create len in
unsafe_blit s ofs r 0l len;
r
end
Note that I changed a lot of places in my code from int -> int32
when I run my code I got an error:
./xsd2coq < grammar/cpf.xsd > coq/cpf.v
Segmentation fault (core dumped)
In the file xsd2coq.ml
I have an buffer with is:
let main () =
let xml = parse_xml stdin in
let xsds = Xsd_of_xml.xsd_of_xml xml in
let b = Buffer.create 10000 in
Coq_of_xsd.genr_ml b xsds;
Buffer.output_buffer stdout b;;
let _ = run main;;
I would like to understand what are the reason that yield the error about segmentation fault? Could you please give me any hints or suggestion to be able to debug my code? Thank you
Upvotes: 0
Views: 1151
Reputation: 66823
Well "%string_length" is an OCaml primitive. You can't change its return type just by changing your OCaml code. You also have to change the code in the OCaml runtime. If OCaml tries to treat an int
value (which is what you get from the runtime) as an int32
value, it will crash. An int32
value is going to be represented by a boxed value (a pointer), but an int
value is an immediate value.
It would be a lot of work to do what you're trying to do. Since strings are quite limited in length (at least in a 32-bit architecture), I'm not sure it will be particularly useful.
Upvotes: 7