diff options
| author | Michael Soegtrop | 2019-12-28 15:18:17 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2019-12-28 15:18:17 +0100 |
| commit | 596515b46d08b470c57eb247e1efdd385acf4f3d (patch) | |
| tree | 2802ad0375510249cf35b43daf762471ed12d216 /dev | |
| parent | f403262aaa9ebe5cf518561875c3a46da83a98b6 (diff) | |
| parent | 00c0b652311b8c6b26c7e21b17db4ab12a35f286 (diff) | |
Merge PR #11323: Fix mulc on 32-bit architectures
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/critical-bugs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 67becb251a..2d187f7bae 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -255,6 +255,18 @@ Conversion machines GH issue number: #9925 risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: broken long multiplication primitive integer emulation layer on 32 bits + introduced: e43b176 + impacted released versions: 8.10.0, 8.10.1, 8.10.2 + impacted development branches: 8.11 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 4e176a7 + found by: Soegtrop, Melquiond + exploit: test-suite/bugs/closed/bug_11321.v + GH issue number: #11321 + risk: critical, as any BigN computation on 32-bit architectures is wrong + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 |