diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 10:03:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-24 10:03:17 +0100 |
| commit | 989553966c7ba1a2cc23fd10fc2633dcb0f98648 (patch) | |
| tree | fa19d67b2fcee5b987fa1f7d2b582b9ca1df17f1 /theories/ZArith/ZArith_base.v | |
| parent | a277da239514ad3bcabc7933a14cfcdc46f272e5 (diff) | |
Fix incorrect long multiplication in the VM.
If the result had its 30th bit set, then all the high part of the result
on a 64-bit architecture would end up being set, thus breaking subsequent
computations.
This patch also fixes the incorrectly parenthesized definition of
uint32_of_value, which by luck was never misused.
Diffstat (limited to 'theories/ZArith/ZArith_base.v')
0 files changed, 0 insertions, 0 deletions