Contracts & Harnesses for NonNull::read, NonNull::read_volatile, NonNull::read_unaligned

[QinyuanWu]

Towards #53

Contracts & Harnesses for NonNull::read, NonNull::read_volatile, NonNull::read_unaligned

Discussion

For the ensures clause in the contract for NonNull::read, I could not directly compare the value pointed by self and result due to unsized and lack of PartialEq implementation, and the comparison is currently moved to the harness.

Verification

Successful verification:

SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.1760525s

Complete - 5 successfully verified harnesses, 0 failures, 5 total.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[QinyuanWu]

Addressed previous PR comments and Increased SIZE:

Checking harness ptr::non_null::verify::non_null_check_read_unaligned...
SUMMARY:
 ** 0 of 261 failed (4 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 18.91408s

Checking harness ptr::non_null::verify::non_null_check_read_volatile...
SUMMARY:
 ** 0 of 237 failed (4 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 15.834378s

Checking harness ptr::non_null::verify::non_null_check_read...
SUMMARY:
 ** 0 of 229 failed (4 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 38.454617s

Complete - 3 successfully verified harnesses, 0 failures, 3 total.

[zhassan-aws]

Looks good. Thanks!

[QinyuanWu]

@zhassan-aws Thank you! Waiting for another review.

[zhassan-aws]

Can you please resolve the conflict?

[Eh2406]

I've then asked to help review this.

[HuStmpHrrr]

LGTM

[QinyuanWu]

@zhassan-aws resolved conflicts and addressed all comments, ready to merge:

VERIFICATION:- SUCCESSFUL
Verification Time: 0.173812s

Complete - 9 successfully verified harnesses, 0 failures, 9 total.

[zhassan-aws]

trigger approval workflow

[zhassan-aws]

trigger approval workflow