From 7b38e4b6ce13cb3c0ee894415e3a2afe00ad7d9b Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 2 Nov 2023 10:56:51 -0400 Subject: [PATCH] symbolic-syntax: Fix README backticks Co-authored-by: Ryan Scott --- symbolic-syntax/README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/symbolic-syntax/README.md b/symbolic-syntax/README.md index 7bbaecd2..dd5dbc93 100644 --- a/symbolic-syntax/README.md +++ b/symbolic-syntax/README.md @@ -11,7 +11,7 @@ The main type addition is for representing pointers: - `Pointer` -Unlike C/C++, these pointers are untyped and essentially correspond to `uint8_t*``. +Unlike C/C++, these pointers are untyped and essentially correspond to `uint8_t*`. There are a few wrappers around `Bitvector` types for portability and convenience: @@ -28,13 +28,13 @@ There are a few wrappers around `Bitvector` types for portability and convenienc 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 ``_`` (for each `i` between `0` and `` - 1`). Note that `t` must be a scalar type (e.g., no nested `Vector`\ s), and `s` and `n` must both be concrete values. +- `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 `_` (for each `i` between `0` and ` - 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-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). - `pointer-eq :: Pointer -> Pointer -> Bool`. -- `pointer-read :: forall (t :: Type) -> Endianness -> Pointer -> t` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)`` (for some positive number `w`) or one of the type aliases listed above. -- `pointer-write :: forall (t :: Type) -> Endianness -> Pointer -> t -> Unit` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)`` (for some positive number `w`) or one of the type aliases listed above. +- `pointer-read :: forall (t :: Type) -> Endianness -> Pointer -> t` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)` (for some positive number `w`) or one of the type aliases listed above. +- `pointer-write :: forall (t :: Type) -> Endianness -> Pointer -> t -> Unit` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)` (for some positive number `w`) or one of the type aliases listed above. [syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax