diff options
| author | Pierre-Marie Pédrot | 2021-03-25 17:23:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-26 12:15:39 +0100 |
| commit | 35c1d9e7add9a415d1406e6bb1eae7bd67ba5357 (patch) | |
| tree | 05ab0584788f59f5e97ffd65049a4a2e7c8eef2e /kernel/vmvalues.mli | |
| parent | 71453f1643b55679d44caee30ce5541b5aa47263 (diff) | |
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.
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index d15595766a..534a85d773 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -148,7 +148,6 @@ val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values val val_of_uint : Uint63.t -> structured_values -val val_of_parray : structured_values Parray.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" |