Skip to content
  • Xavier Leroy's avatar
    Truncation of array sizes when converting them to Coq's Z type · de0ff0bc
    Xavier Leroy authored
    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)
    de0ff0bc