aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-06-09 20:35:55 +0200
committerGuillaume Melquiond2020-06-09 20:35:55 +0200
commit95be052f60b1b6b4cc0b12e92b3d1b86b5bd7ca9 (patch)
tree12e87cc010637051271423455d5b1bf42269215b /dev
parent95fb6a9e62bc061db5c9fe39a25d69b7cf2cd06e (diff)
parent9c76e6b4c9ae24826668fa9f72faf93e5d4c6acf (diff)
Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.leb
Ack-by: Zimmi48 Reviewed-by: erikmd Reviewed-by: silene
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.