diff options
| author | Maxime Dénès | 2019-04-29 15:32:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-29 15:32:55 +0200 |
| commit | 8ca2f91c5594c88abeab764d5c0f04ce16930abb (patch) | |
| tree | ed700d30176ef4c3e83f08968f9dca4fb972df0c /dev | |
| parent | deb962b17448e22ba00cba24d2e77654b8406041 (diff) | |
| parent | 4ae7e833ff1ddf2db503c1d3a49172d36575a142 (diff) | |
Merge PR #9925: [vm] Protect accu and coq_env
Ack-by: Zimmi48
Reviewed-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
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 f532e1b68f..01c2b574a2 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 |