diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-02-04 17:03:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-02-08 17:11:46 +0100 |
| commit | de0ff0bcb9df3dba542d22336e58e70ba8bda947 (patch) | |
| tree | 67e483aa162f6d21948cbcf18448322459d5d3b3 /x86 | |
| parent | f80498e19a670040dce0795a8ea1cc83ca490ecc (diff) | |
| download | compcert-de0ff0bcb9df3dba542d22336e58e70ba8bda947.tar.gz compcert-de0ff0bcb9df3dba542d22336e58e70ba8bda947.zip | |
Truncation of array sizes when converting them to Coq's Z type
The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST. However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32. This is not correct, esp. on a 64-bit target.
This commit refactors C2C around three integer conversion functions:
convertInt32 producing a Coq "int" (32 bit)
convertInt64 producing a Coq "int64" (64 bit)
convertIntZ producing a Coq "Z" (arbitrary precision)
Diffstat (limited to 'x86')
0 files changed, 0 insertions, 0 deletions