diff options
author | Son Ho | 2022-01-26 09:02:22 +0100 |
---|---|---|
committer | Son Ho | 2022-01-26 09:02:22 +0100 |
commit | 7372a2fb529df9750b06ccefdbb3f716f9823846 (patch) | |
tree | 45557d0be5c548fc87133ac43447db0fe8f79b7c /src/Values.ml | |
parent | 6873d0b2e3bc43c936d4ac047f7903dfe93f6ce9 (diff) |
Replace other occurrences of mvalue with msymbolic_value
Diffstat (limited to 'src/Values.ml')
-rw-r--r-- | src/Values.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Values.ml b/src/Values.ml index 45bd5b6e..90250c63 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -195,12 +195,18 @@ type mvalue = typed_value [@@deriving show] Note that we never automatically visit the meta-values with the visitors: they really are meta information, and shouldn't be considered as part of the environment during a symbolic execution. + + TODO: we may want to create wrappers, to prevent mixing meta values + and regular values. *) type msymbolic_value = symbolic_value [@@deriving show] (** "Meta"-symbolic value. See the explanations for [mvalue] + + TODO: we may want to create wrappers, to prevent mixing meta values + and regular values. *) (** When giving shared borrows to functions (i.e., inserting shared borrows inside @@ -645,7 +651,7 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) - | AEndedMutBorrow of mvalue * typed_avalue + | AEndedMutBorrow of msymbolic_value * typed_avalue (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value that we gave back as a meta-value, to help with the synthesis. We also remember the child [avalue] because this structural information @@ -656,7 +662,7 @@ and aborrow_content = | AEndedIgnoredMutBorrow of { child : typed_avalue; given_back_loans_proj : typed_avalue; - given_back_meta : mvalue; + given_back_meta : msymbolic_value; (** [given_back_meta] is used to store the (symbolic) value we gave back upon ending the borrow. |