Skip to content

Commit 2640cd5

Browse files
authored
small edit
Added note about verification challenge criteria.
1 parent 68d06ea commit 2640cd5

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

doc/src/challenges/0028-flt2dec.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,10 @@ For functions taking inputs of generic type 'T', the proofs can be limited to pr
4646
*List of UBs*
4747

4848
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
49-
5049
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
5150
* Invoking undefined behavior via compiler intrinsics.
5251
* Mutating immutable bytes.
5352
* Producing an invalid value.
53+
54+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
55+
in addition to the ones listed above.

0 commit comments

Comments
 (0)