Merge pull request #1752 from GaloisInc/heapster-docfixes

Minor Heapster docfixes

heapster-saw/doc/Permissions.md

@@ -13,8 +13,8 @@ In this document, we use the following metavariables to refer to different sorts
   `sh`               | Shape expression
   `l`                | Lifetime expression
   `p`                | Value permission
-                     
-                     
+
+
 
 Value Types
 ================
@@ -71,8 +71,8 @@ In addition to the above expressions, we also have shape expressions, which we s
 | `sh1 orsh sh2`              | `llvmshape w` | A disjunctive shape. `sh1` and `sh2` need not have the same size. |
 | `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(sz,p)`             | `llvmshape w` | Like `fieldsh(p)`, but where the permission acts on a pointer of size `sz`. |
+| `fieldsh(sz,p)`             | `llvmshape w` | A shape for a single pointer field, given a permission `p` that acts on a pointer of size `sz`. |
+| `fieldsh(p)`                | `llvmshape w` | Equivalent to `fieldsh(w,p)`. |
 | `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 |
 | `falsesh`                    | `llvmshape w` | The unsatisfiable or contradictory shape |

src/SAWScript/Interpreter.hs

@@ -4060,15 +4060,15 @@ primitives = Map.fromList
     "HeapsterEnv -> String -> String -> String -> TopLevel HeapsterEnv"
     (bicVal heapster_assume_fun)
     Experimental
-    [ "heapster_assume_fun nm perms trans assumes that function nm has"
+    [ "heapster_assume_fun env nm perms trans assumes that function nm has"
     , " permissions perms and translates to the SAW core term trans"
     ]
 
   , prim "heapster_assume_fun_rename"
     "HeapsterEnv -> String -> String -> String -> String -> TopLevel HeapsterEnv"
     (bicVal heapster_assume_fun_rename)
     Experimental
-    [ "heapster_assume_fun_rename nm nm_t perms trans assumes that function nm"
+    [ "heapster_assume_fun_rename env nm nm_to perms trans assumes that function nm"
     , " has permissions perms and translates to the SAW core term trans. If"
     , " trans is not an identifier then it is bound to the defined name nm_to."
     ]
@@ -4078,15 +4078,15 @@ primitives = Map.fromList
     (bicVal heapster_assume_fun_rename_prim)
     Experimental
     [
-      "heapster_assume_fun_rename_prim nm nm_to perms assumes that function nm"
+      "heapster_assume_fun_rename_prim env nm nm_to perms assumes that function nm"
     , " has permissions perms as a primitive."
     ]
 
   , prim "heapster_assume_fun_multi"
     "HeapsterEnv -> String -> [(String, String)] -> TopLevel HeapsterEnv"
     (bicVal heapster_assume_fun_multi)
     Experimental
-    [ "heapster_assume_fun_multi nm [(perm1, trans1), ...] assumes that function"
+    [ "heapster_assume_fun_multi env nm [(perm1, trans1), ...] assumes that function"
     , " nm can be typed with 0 or more permissions, each with the corresponding"
     , " translation to SAW core"
     ]