From 35c1d9e7add9a415d1406e6bb1eae7bd67ba5357 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Mar 2021 17:23:03 +0100
Subject: Never store persistent arrays as VM structured values.

Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.

There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.

Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
---
 test-suite/bugs/closed/bug_14006.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_14006.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_14006.v b/test-suite/bugs/closed/bug_14006.v
new file mode 100644
index 0000000000..b857959ae9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14006.v
@@ -0,0 +1,3 @@
+From Coq Require Import Int63 PArray.
+Definition t : array nat := [| 1; 3; 2 | 4 |].
+Definition vm_accu_set v := Eval vm_compute in t.[1 <- v].
-- 
cgit v1.2.3