From 7ff8b12c14867e43d54c3d4c8976a6179250893d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 25 Mar 2021 15:03:03 +0100
Subject: Document as critical.

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

(limited to 'dev')

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 4452baf513..5c8b8944a7 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -344,6 +344,16 @@ Conversion machines
         noticeable if activated by chance, since it usually breaks
         control-flow integrity
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: arbitrary code execution on irreducible PArray.set
+  introduced: 8.13
+  impacted released versions: 8.13.0, 8.13.1
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 8.13.2
+  found by: Melquiond
+  GH issue number: #13998
+  risk: none, unless using primitive array operations; systematic otherwise
+
 Side-effects
 
   component: side-effects
-- 
cgit v1.2.3