Skip to content

Commit

Permalink
Update Permissions.md (#1529)
Browse files Browse the repository at this point in the history
Size comes first on fieldsh
  • Loading branch information
jpaykin authored Dec 2, 2021
1 parent 04a599b commit a87ed23
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion heapster-saw/doc/Permissions.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ In addition to the above expressions, we also have shape expressions, which we s
| `sh1 ; sh2` | `llvmshape w` | A sequence of two shapes |
| `[l]ptrsh(rw,sh)` | `llvmshape w` | A shape for a pointer to another memory block, i.e. a memblock permission, with a given shape. This memblock permission will have the same read/write and lifetime modalities as the memblock permission containing this pointer shape, unless they are specifically overridden by the pointer shape; i.e., we have that `[l]memblock(rw,off,len,[l']ptrsh(rw',sh)) = [l]memblock(rw,off,len, fieldsh([l']memblock(rw',0,len(sh),sh)))`, where `rw'` and/or `l'` can be `Nothing`, in which case they default to `rw` and `l`, respectively. |
| `fieldsh(p)` | `llvmshape w` | A shape for a single pointer field, given a permission that acts on a pointer of unknown size. |
| `fieldsh(p,sz)` | `llvmshape w` | Like `fieldsh(p)`, but where the permission acts on a pointer of size `sz`. |
| `fieldsh(sz,p)` | `llvmshape w` | Like `fieldsh(p)`, but where the permission acts on a pointer of size `sz`. |
| `arraysh(s,len,sh)` | `llvmshape w` | A shape for an array with the given stride, length (in number of elements = total length / stride), and fields `sh` |
| `exsh x:a.sh` | `llvmshape w` | An existential shape |

Expand Down

0 comments on commit a87ed23

Please sign in to comment.