symbolic-syntax: make-null -> pointer-make-null

symbolic-syntax/README.md

@@ -29,7 +29,7 @@ The extra operations are:
 
 - `bv-typed-literal :: Type -> Integer -> Bitvector w` where the first argument is a `Bitvector` type alias (see the Types section), the second argument is the value the `Bitvector` should contain, and `w` is the number of bits in the returned `Bitvector` (will match the width of the `Type` argument).
 - `fresh-vec :: String Unicode -> forall (t :: Type) -> Nat -> Vector t`, where `(fresh-vec s t n)` generates a length-`n` vector where each element is a fresh constant of type `t` with the name `<s>_<i>` (for each `i` between `0` and `<n> - 1`). Note that `t` must be a scalar type (e.g., no nested `Vector`\ s), and `s` and `n` must both be concrete values.
-- `make-null :: Pointer` returns a null pointer.
+- `pointer-make-null :: Pointer` returns a null pointer.
 - `pointer-add :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).
 - `pointer-diff :: Pointer -> Pointer -> Bitvector w` where `w` is the number of bits in a pointer (usually 32 or 64).
 - `pointer-sub :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).

symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs

@@ -362,7 +362,7 @@ wrapPointerDiff = ExtensionWrapper
 
 -- | Wrapper for 'DMS.MacawNullPtr' to construct a null pointer.
 --
--- > make-null
+-- > pointer-make-null
 wrapMakeNull
   :: ( w ~ DMC.ArchAddrWidth arch
      , 1 <= w
@@ -372,7 +372,7 @@ wrapMakeNull
                       Ctx.EmptyCtx
                       (LCLM.LLVMPointerType w)
 wrapMakeNull = ExtensionWrapper
-  { extName = LCSA.AtomName "make-null"
+  { extName = LCSA.AtomName "pointer-make-null"
   , extArgTypes = Ctx.empty
   , extWrapper = \_ ->
       let nullptr = DMS.MacawNullPtr (DMC.addrWidthRepr WI.knownNat) in
@@ -577,7 +577,7 @@ extensionWrappers = Map.fromList
   , (LCSA.AtomName "pointer-diff", SomeExtensionWrapper wrapPointerDiff)
   , (LCSA.AtomName "pointer-sub", SomeExtensionWrapper wrapPointerSub)
   , (LCSA.AtomName "pointer-eq", SomeExtensionWrapper wrapPointerEq)
-  , (LCSA.AtomName "make-null", SomeExtensionWrapper wrapMakeNull)
+  , (LCSA.AtomName "pointer-make-null", SomeExtensionWrapper wrapMakeNull)
   ]
 
 ptrTypeParser :: LCSE.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)

symbolic-syntax/test-data/ops.cbl

@@ -3,7 +3,7 @@
   (start start:
     (let b (bv-typed-literal SizeT 42))
     (let v (fresh-vec "v" Short 7))
-    (let n (make-null))
+    (let n (pointer-make-null))
     (let d (pointer-diff p q))
     (let r (pointer-add p d))
 	(let s (pointer-sub r d))

symbolic-syntax/test-data/ops.out

@@ -2,7 +2,7 @@
    (start start:
       (let b (bv-typed-literal SizeT 42))
       (let v (fresh-vec "v" Short 7))
-      (let n (make-null))
+      (let n (pointer-make-null))
       (let d (pointer-diff p q))
       (let r (pointer-add p d))
       (let s (pointer-sub r d))

symbolic-syntax/test-data/ops.out.good

@@ -2,7 +2,7 @@
    (start start:
       (let b (bv-typed-literal SizeT 42))
       (let v (fresh-vec "v" Short 7))
-      (let n (make-null))
+      (let n (pointer-make-null))
       (let d (pointer-diff p q))
       (let r (pointer-add p d))
       (let s (pointer-sub r d))