We've encounterd embedded programs that carve out large static arrays ... and they compile and run correctly, but CIL can't process them because the array's are too big.
In particular, CIL appears to use an OCaml int for an array size, but since OCaml int's are 1) signed 2) 1-bit shorter than machine ints to facilitate fast garbage collection; it is possible - and we do - have arrays with a size that is bigger than can be represented with an OCaml int.
Natrually this is a problem in practice only on 32-bit builds, but since all the pre-combiled Windows OCaml builds are 32-bit the problem occurs.
I believe this to be the cause because if I set the size to be one byte smaller than the largest 2s complement number representable in 31 bits it works.
Now, "morally", CIL should be able to process any C file that the compiler can process - but on a 32-bit machine this does break down here. I expect the right thing to do would be to modify CIL to use Nativeint library for storying array sizes.
Log in to post a comment.