Skip to content
Snippets Groups Projects
Commit 7d0b39f2 authored by Arthur Azevedo de Amorim's avatar Arthur Azevedo de Amorim
Browse files

Fix argument order in comment.

parent 3fd5a5d0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/gen_heap.v
+ 1
− 1
View file @ 7d0b39f2
...@@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to ...@@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
locations. This is done as follows: locations. This is done as follows:
- When one allocates a location, in addition to the point-to connective [l ↦ v], - When one allocates a location, in addition to the point-to connective [l ↦ v],
one also obtains the token [meta_token ⊤ l]. This token is an exclusive one also obtains the token [meta_token l ⊤]. This token is an exclusive
resource that denotes that no meta data has been associated with the resource that denotes that no meta data has been associated with the
namespaces in the mask [⊤] for the location [l]. namespaces in the mask [⊤] for the location [l].
- Meta data tokens can be split w.r.t. namespace masks, i.e. - Meta data tokens can be split w.r.t. namespace masks, i.e.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment