diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-13 14:04:49 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-13 14:04:49 +0100 |
commit | 4d7a6709946a0c30e932c00405252b42e348eb64 (patch) | |
tree | aca0e5450b17c0c5443800c30a9e0919fde856d1 /lib/Responsefile.mli | |
parent | 1c477f375f20e882b429175c737ad013ff202c0b (diff) | |
download | compcert-4d7a6709946a0c30e932c00405252b42e348eb64.tar.gz compcert-4d7a6709946a0c30e932c00405252b42e348eb64.zip |
Print size argument of Init_space as Z not as int32
Init_space has an argument of type Z and it can exceed the range of a 32-bit integer.
Reported by Frédéric Besson.
Diffstat (limited to 'lib/Responsefile.mli')
0 files changed, 0 insertions, 0 deletions