You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Dec 2, 2023. It is now read-only.
Scopes does not segregate unsafe and safe code, and consequently does not provide any way of proving whether a particular function invokes unsafe code. A new keyword unsafe must be added, which defines a region of code that allows unsafe operations, and then the prover must be augmented to tag every single potentially unsafe operation. If these operations occur outside an unsafe context, a compiler error should be generated.
The text was updated successfully, but these errors were encountered:
Scopes does not segregate unsafe and safe code, and consequently does not provide any way of proving whether a particular function invokes unsafe code. A new keyword
unsafe
must be added, which defines a region of code that allows unsafe operations, and then the prover must be augmented to tag every single potentially unsafe operation. If these operations occur outside an unsafe context, a compiler error should be generated.The text was updated successfully, but these errors were encountered: