From: Ralf Jung Date: Wed, 19 Jul 2017 20:55:23 +0000 (-0700) Subject: mention boxes X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/ef943c44bdd6f451b65b49b81f17a5a339aad5ec?ds=inline;hp=d7f72237fdbfb0771307c1e3c4a4d2e053857b9c mention boxes --- diff --git a/personal/_posts/2017-07-17-types-as-contracts.md b/personal/_posts/2017-07-17-types-as-contracts.md index 6bcaea0..bb867e7 100644 --- a/personal/_posts/2017-07-17-types-as-contracts.md +++ b/personal/_posts/2017-07-17-types-as-contracts.md @@ -283,11 +283,11 @@ For compound types like tuples, `struct` or `enum`, validation proceeds recursiv In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type). However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here. -Finally, at a reference type, two things happen. -First, the reference itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer. -The reference is also checked to be non-NULL and properly aligned for the type it points to. -Furthermore, validation proceeds recursively after *dereferencing* the reference. -Crucially, the `mutbl` and `lft` for this recursive call are taking the reference type into account: +Finally, when encountering a box or reference type, two things happen. +First, the pointer itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer. +The pointer is also checked to be non-NULL and properly aligned for the type it points to. +Furthermore, validation proceeds recursively after *dereferencing* the pointer. +Crucially, for the case of validating a reference, the `mutbl` and `lft` for this recursive call are taking the type into account: If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime. If `mutbl` was mutable, it becomes immutable when following a shared reference.