Skip to content

Commit

Permalink
Merge PR coq#19192: Change critical bug conversion machine classifica…
Browse files Browse the repository at this point in the history
…tion 15070 to also affecting native

Reviewed-by: proux01
Co-authored-by: proux01 <[email protected]>
  • Loading branch information
coqbot-app[bot] and proux01 authored Jun 9, 2024
2 parents 054e150 + ae3065e commit 5b40bec
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions dev/doc/critical-bugs.md
Original file line number Diff line number Diff line change
Expand Up @@ -595,10 +595,10 @@ For instance `α` and `__U03b1_` were the same in the native compiler.

#### arbitrary code execution on arrays of floating point numbers

- component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
- component: "virtual" and "native" conversion machines
- introduced: 8.13
- impacted released versions: 8.13.0, 8.13.1, 8.14.0
- impacted coqchk versions: none (no virtual machine in coqchk)
- impacted coqchk versions: none (no VM / native computation in coqchk)
- fixed in: 8.14.1
- found by: Melquiond
- GH issue number: coq/coq#15070
Expand Down

0 comments on commit 5b40bec

Please sign in to comment.