Merge PR #9837: Fix some critical-bugs informations

Reviewed-by: Zimmi48

2 files changed, 280 insertions, 8 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 8d78559c0d..c0a5b9095c 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -63,8 +63,8 @@ Typing constructions
   impacted coqchk versions: ?
   fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
   found by: Georgi Guninski
-  exploit: test-suite/bugs/closed/4294.v
-  GH issue number: #4294
+  exploit: test-suite/failure/prop_set_proof_irrelevance.v
+  GH issue number: none?
   risk: ?
 
 Module system
@@ -77,7 +77,7 @@ Module system
   impacted coqchk versions: ?
   fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
   found by: Dénès
-  exploit: test-suite/bugs/closed/4294.v
+  exploit: test-suite/bugs/closed/bug_4294.v
   GH issue number: #4294
   risk: ?
 
@@ -105,7 +105,7 @@ Universes
   impacted coqchk versions: ?
   fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), 
   found by: Barras
-  exploit: test-suite/failure/inductive4.v
+  exploit: test-suite/failure/inductive.v
   GH issue number: none
   risk: unlikely to be activated by chance
 
@@ -141,7 +141,7 @@ Primitive projections
   impacted coqchk versions: ?
   fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
   found by: Dénès exploiting bug #4588
-  exploit: test-suite/bugs/closed/4588.v
+  exploit: test-suite/bugs/closed/bug_4588.v
   GH issue number: #4588
   risk: ?
 
@@ -167,7 +167,7 @@ Conversion machines
   impacted coqchk versions: none (no virtual machine in coqchk)
   fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
   found by: Dénès, Pédrot
-  exploit: test-suite/failure/vm-bug4157.v
+  exploit: test-suite/bugs/closed/bug_4157.v
   GH issue number: #4157
   risk: 
 
@@ -179,7 +179,7 @@ Conversion machines
   impacted coqchk versions: none (no virtual machine in coqchk)
   fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
   found by: Dénès
-  exploit: test-suite/bugs/closed/6677.v
+  exploit: test-suite/bugs/closed/bug_6677.v
   GH issue number: #6677
   risk: 
 
@@ -203,7 +203,7 @@ Conversion machines
   impacted coqchk versions: none (no native computation in coqchk)
   fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), 
   found by: Letouzey, Dénès
-  exploit: lost?
+  exploit: see commit message for 244d7a9aa
   GH issue number: ?
   risk: 
 
diff --git a/test-suite/bugs/closed/bug_4157.v b/test-suite/bugs/closed/bug_4157.v
new file mode 100644
index 0000000000..a9e96fcdde
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4157.v
@@ -0,0 +1,272 @@
+(** The following proof is due to a bug in `vm_compute` and was found by
+    Maxime Dénès and Pierre-Marie Pédrot. *)
+Inductive t :=
+| C_0 : nat -> t
+| C_1 : nat -> t
+| C_2 : nat -> t
+| C_3 : nat -> t
+| C_4 : nat -> t
+| C_5 : nat -> t
+| C_6 : nat -> t
+| C_7 : nat -> t
+| C_8 : nat -> t
+| C_9 : nat -> t
+| C_10 : nat -> t
+| C_11 : nat -> t
+| C_12 : nat -> t
+| C_13 : nat -> t
+| C_14 : nat -> t
+| C_15 : nat -> t
+| C_16 : nat -> t
+| C_17 : nat -> t
+| C_18 : nat -> t
+| C_19 : nat -> t
+| C_20 : nat -> t
+| C_21 : nat -> t
+| C_22 : nat -> t
+| C_23 : nat -> t
+| C_24 : nat -> t
+| C_25 : nat -> t
+| C_26 : nat -> t
+| C_27 : nat -> t
+| C_28 : nat -> t
+| C_29 : nat -> t
+| C_30 : nat -> t
+| C_31 : nat -> t
+| C_32 : nat -> t
+| C_33 : nat -> t
+| C_34 : nat -> t
+| C_35 : nat -> t
+| C_36 : nat -> t
+| C_37 : nat -> t
+| C_38 : nat -> t
+| C_39 : nat -> t
+| C_40 : nat -> t
+| C_41 : nat -> t
+| C_42 : nat -> t
+| C_43 : nat -> t
+| C_44 : nat -> t
+| C_45 : nat -> t
+| C_46 : nat -> t
+| C_47 : nat -> t
+| C_48 : nat -> t
+| C_49 : nat -> t
+| C_50 : nat -> t
+| C_51 : nat -> t
+| C_52 : nat -> t
+| C_53 : nat -> t
+| C_54 : nat -> t
+| C_55 : nat -> t
+| C_56 : nat -> t
+| C_57 : nat -> t
+| C_58 : nat -> t
+| C_59 : nat -> t
+| C_60 : nat -> t
+| C_61 : nat -> t
+| C_62 : nat -> t
+| C_63 : nat -> t
+| C_64 : nat -> t
+| C_65 : nat -> t
+| C_66 : nat -> t
+| C_67 : nat -> t
+| C_68 : nat -> t
+| C_69 : nat -> t
+| C_70 : nat -> t
+| C_71 : nat -> t
+| C_72 : nat -> t
+| C_73 : nat -> t
+| C_74 : nat -> t
+| C_75 : nat -> t
+| C_76 : nat -> t
+| C_77 : nat -> t
+| C_78 : nat -> t
+| C_79 : nat -> t
+| C_80 : nat -> t
+| C_81 : nat -> t
+| C_82 : nat -> t
+| C_83 : nat -> t
+| C_84 : nat -> t
+| C_85 : nat -> t
+| C_86 : nat -> t
+| C_87 : nat -> t
+| C_88 : nat -> t
+| C_89 : nat -> t
+| C_90 : nat -> t
+| C_91 : nat -> t
+| C_92 : nat -> t
+| C_93 : nat -> t
+| C_94 : nat -> t
+| C_95 : nat -> t
+| C_96 : nat -> t
+| C_97 : nat -> t
+| C_98 : nat -> t
+| C_99 : nat -> t
+| C_100 : nat -> t
+| C_101 : nat -> t
+| C_102 : nat -> t
+| C_103 : nat -> t
+| C_104 : nat -> t
+| C_105 : nat -> t
+| C_106 : nat -> t
+| C_107 : nat -> t
+| C_108 : nat -> t
+| C_109 : nat -> t
+| C_110 : nat -> t
+| C_111 : nat -> t
+| C_112 : nat -> t
+| C_113 : nat -> t
+| C_114 : nat -> t
+| C_115 : nat -> t
+| C_116 : nat -> t
+| C_117 : nat -> t
+| C_118 : nat -> t
+| C_119 : nat -> t
+| C_120 : nat -> t
+| C_121 : nat -> t
+| C_122 : nat -> t
+| C_123 : nat -> t
+| C_124 : nat -> t
+| C_125 : nat -> t
+| C_126 : nat -> t
+| C_127 : nat -> t
+| C_128 : nat -> t
+| C_129 : nat -> t
+| C_130 : nat -> t
+| C_131 : nat -> t
+| C_132 : nat -> t
+| C_133 : nat -> t
+| C_134 : nat -> t
+| C_135 : nat -> t
+| C_136 : nat -> t
+| C_137 : nat -> t
+| C_138 : nat -> t
+| C_139 : nat -> t
+| C_140 : nat -> t
+| C_141 : nat -> t
+| C_142 : nat -> t
+| C_143 : nat -> t
+| C_144 : nat -> t
+| C_145 : nat -> t
+| C_146 : nat -> t
+| C_147 : nat -> t
+| C_148 : nat -> t
+| C_149 : nat -> t
+| C_150 : nat -> t
+| C_151 : nat -> t
+| C_152 : nat -> t
+| C_153 : nat -> t
+| C_154 : nat -> t
+| C_155 : nat -> t
+| C_156 : nat -> t
+| C_157 : nat -> t
+| C_158 : nat -> t
+| C_159 : nat -> t
+| C_160 : nat -> t
+| C_161 : nat -> t
+| C_162 : nat -> t
+| C_163 : nat -> t
+| C_164 : nat -> t
+| C_165 : nat -> t
+| C_166 : nat -> t
+| C_167 : nat -> t
+| C_168 : nat -> t
+| C_169 : nat -> t
+| C_170 : nat -> t
+| C_171 : nat -> t
+| C_172 : nat -> t
+| C_173 : nat -> t
+| C_174 : nat -> t
+| C_175 : nat -> t
+| C_176 : nat -> t
+| C_177 : nat -> t
+| C_178 : nat -> t
+| C_179 : nat -> t
+| C_180 : nat -> t
+| C_181 : nat -> t
+| C_182 : nat -> t
+| C_183 : nat -> t
+| C_184 : nat -> t
+| C_185 : nat -> t
+| C_186 : nat -> t
+| C_187 : nat -> t
+| C_188 : nat -> t
+| C_189 : nat -> t
+| C_190 : nat -> t
+| C_191 : nat -> t
+| C_192 : nat -> t
+| C_193 : nat -> t
+| C_194 : nat -> t
+| C_195 : nat -> t
+| C_196 : nat -> t
+| C_197 : nat -> t
+| C_198 : nat -> t
+| C_199 : nat -> t
+| C_200 : nat -> t
+| C_201 : nat -> t
+| C_202 : nat -> t
+| C_203 : nat -> t
+| C_204 : nat -> t
+| C_205 : nat -> t
+| C_206 : nat -> t
+| C_207 : nat -> t
+| C_208 : nat -> t
+| C_209 : nat -> t
+| C_210 : nat -> t
+| C_211 : nat -> t
+| C_212 : nat -> t
+| C_213 : nat -> t
+| C_214 : nat -> t
+| C_215 : nat -> t
+| C_216 : nat -> t
+| C_217 : nat -> t
+| C_218 : nat -> t
+| C_219 : nat -> t
+| C_220 : nat -> t
+| C_221 : nat -> t
+| C_222 : nat -> t
+| C_223 : nat -> t
+| C_224 : nat -> t
+| C_225 : nat -> t
+| C_226 : nat -> t
+| C_227 : nat -> t
+| C_228 : nat -> t
+| C_229 : nat -> t
+| C_230 : nat -> t
+| C_231 : nat -> t
+| C_232 : nat -> t
+| C_233 : nat -> t
+| C_234 : nat -> t
+| C_235 : nat -> t
+| C_236 : nat -> t
+| C_237 : nat -> t
+| C_238 : nat -> t
+| C_239 : nat -> t
+| C_240 : nat -> t
+| C_241 : nat -> t
+| C_242 : nat -> t
+| C_243 : nat -> t
+| C_244 : nat -> t
+| C_245 : nat -> t
+| C_246 : nat -> t
+| C_247 : nat -> t
+| C_248 : nat -> t
+| C_249 : nat -> t
+| C_250 : nat -> t
+| C_251 : nat -> t
+| C_252 : nat -> t
+| C_253 : nat -> t
+| C_254 : nat -> t
+| C_255 : nat -> t
+| C_256 : nat -> t.
+
+Definition is_256 (x : t) : bool :=
+  match x with
+  | C_256 _ => true
+  | _ => false
+  end.
+
+Lemma falso : False.
+  assert (is_256 (C_256 0) = true) by reflexivity.
+  (* The next line was successful in 8.2pl3 *)
+  Fail assert (is_256 (C_256 0) = false) by (vm_compute; reflexivity).
+Abort.