diff options
| author | Pierre Roux | 2019-04-12 16:24:56 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-15 16:50:40 +0200 |
| commit | 4ae7e833ff1ddf2db503c1d3a49172d36575a142 (patch) | |
| tree | 8c805aee675a1712d2bf90c373b2bd9c0aee33c1 /dev | |
| parent | 591431312465291e85fb352a69e947eedeb2e199 (diff) | |
Update critical-bugs
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 c0a5b9095c..c23d2fb528 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -195,6 +195,18 @@ Conversion machines GH issue number: ? risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: primitive integer emulation layer on 32 bits not robust to garbage collection + introduced: master (before v8.10 in GH pull request #6914) + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: + found by: Roux, Melquiond + exploit: + GH issue number: #9925 + risk: + 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 |