From 4ae7e833ff1ddf2db503c1d3a49172d36575a142 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 12 Apr 2019 16:24:56 +0200
Subject: Update critical-bugs

---
 dev/doc/critical-bugs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3