From c150f3ab8dc9d1824d88b6fb9b1da14cb544ffc7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 17 Feb 2021 09:53:26 +0100
Subject: Add an entry to file 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 79c2155823..4452baf513 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -332,6 +332,18 @@ Conversion machines
   GH issue number: ocaml/ocaml#6385, #11170
   risk: unlikely to be activated by chance, might happen for autogenerated code
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: buffer overflow, arbitrary code execution on floating-point operations
+  introduced: 8.13
+  impacted released versions: 8.13.0
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 8.13.1
+  found by: Melquiond
+  GH issue number: #13867
+  risk: none, unless using floating-point operations; high otherwise;
+        noticeable if activated by chance, since it usually breaks
+        control-flow integrity
+
 Side-effects
 
   component: side-effects
-- 
cgit v1.2.3