aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Roux2020-06-09 11:36:41 +0200
committerPierre Roux2020-06-09 15:05:55 +0200
commit9c76e6b4c9ae24826668fa9f72faf93e5d4c6acf (patch)
tree54eacc2828195328ded106c80a94d1dd6a999967 /dev
parent8ecdb858a416b945fd9bc429e9eecf8aa451f0e7 (diff)
Update dev/doc/critical-bugs
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/critical-bugs10
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 3260040248..066facd5db 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -347,6 +347,16 @@ Conflicts with axioms in library
GH issue number: none
risk:
+ component: primitive floating-points
+ summary: Incorrect specification of PrimFloat.leb
+ introduced: 8.11
+ impacted released versions: 8.11.0, 8.11.1, 8.11.2
+ fixed by fixing the spec: #12484
+ found by: Pierre Roux
+ exploit: test-suite/bugs/closed/bug_12483.v
+ GH issue number: #12483
+ risk: proof of false when using the incorrect axiom
+
There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.