diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-09 14:23:03 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-09 14:23:03 +0200 |
| commit | 46e5d165e6277d7502fe4a45e8765526a1117414 (patch) | |
| tree | b22a5dbe1614196cd6d9302f46d36296d3b6865a /driver/Driver.ml | |
| parent | e9c136508ee6e51f26d280ac17370d724b05bf41 (diff) | |
| download | compcert-46e5d165e6277d7502fe4a45e8765526a1117414.tar.gz compcert-46e5d165e6277d7502fe4a45e8765526a1117414.zip | |
More efficient test for powers of two
The previous implementation used to build the full powers-of-two decomposition
of the number. The present implementation recognizes powers of two directly,
then takes the log2.
Diffstat (limited to 'driver/Driver.ml')
0 files changed, 0 insertions, 0 deletions