diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-16 17:56:06 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 11:32:28 +0200 |
commit | 03f39523094fd41c8aad5ee7a8169ffc448cfd4a (patch) | |
tree | f59f6951f244261d8ef38a77860f6feff33a4880 /flocq/Core/Fcore_float_prop.v | |
parent | e036d68cb41de1ddac47d7686d25904281405ffe (diff) | |
download | compcert-03f39523094fd41c8aad5ee7a8169ffc448cfd4a.tar.gz compcert-03f39523094fd41c8aad5ee7a8169ffc448cfd4a.zip |
Read the whole source C file into memory instad of reading it on demand.
Having the file in memory will help build an error message.
Also, this may be slightly faster.
Diffstat (limited to 'flocq/Core/Fcore_float_prop.v')
0 files changed, 0 insertions, 0 deletions