diff options
author | Son Ho | 2022-01-05 10:13:13 +0100 |
---|---|---|
committer | Son Ho | 2022-01-05 10:13:13 +0100 |
commit | f204e2a5543257e77a4bc6ed666efa2f3c4ffabf (patch) | |
tree | eb2a3bfb53c19eace0e10dbf78b5a08679a5e6f0 | |
parent | cc3e866f4a354c6e305bd9737dd46b0648e172af (diff) |
Add comments about symbolic values
-rw-r--r-- | src/Values.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Values.ml b/src/Values.ml index 8ecf8849..a0bd96c5 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -54,10 +54,13 @@ type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } - a projector on loans may see a symbolic value of id `sid` as having type `T` - a projector on borrows may see it as having type `&mut T` We need to make this clear and more consistant. - So [symbolic_value] is actually a projector. TODO: rename + So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj]. + The kind of projector will then depend on the context. *) -(** TODO: make it clear that complementary projectors are projectors on borrows *) +(** TODO: make it clear that complementary projectors are projectors on borrows. + ** TODO: actually this is useless: the set of ended regions should be global! + ** (and thus stored in the context) *) type symbolic_proj_comp = { svalue : symbolic_value; (** The symbolic value itself *) rset_ended : RegionId.set_t; |