diff options
| author | Son Ho | 2022-04-21 12:50:37 +0200 |
|---|---|---|
| committer | Son Ho | 2022-04-21 12:50:37 +0200 |
| commit | 0f2ce5dd56dc1001d5ba7128e6f0ac83ea499267 (patch) | |
| tree | af82e0a05d9a1b37bb50248f6d1b2efa2fb3463f /src/SymbolicToPure.ml | |
| parent | 9cda6b33d667b861f371e89e7cccaf43135cfc7a (diff) | |
Cleanup and update comments
Diffstat (limited to 'src/SymbolicToPure.ml')
| -rw-r--r-- | src/SymbolicToPure.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 65bdcf9c..e32e28d6 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -640,7 +640,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (translate mv).value | V.InactivatedMutBorrow (mv, _) -> (* Same as for shared borrows. However, note that we use inactivated borrows - * only in meta-data: a value actually used in the translation can't come + * only in meta-data: a value actually *used in the translation* can't come * from an unpromoted inactivated borrow *) (translate mv).value | V.MutBorrow (_, v) -> @@ -1451,8 +1451,6 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression option) : fun_decl = - (* Reset the counters *) - reset_pure_counters (); (* Translate *) let def = ctx.fun_decl in let bid = ctx.bid in |