Skip to content

Commit

Permalink
symbolic-syntax: Fix README backticks
Browse files Browse the repository at this point in the history
Co-authored-by: Ryan Scott <rscott@galois.com>
  • Loading branch information
langston-barrett and RyanGlScott authored Nov 2, 2023
1 parent 19f0a57 commit 7b38e4b
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions symbolic-syntax/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand All @@ -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 ``<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.
- `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-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

0 comments on commit 7b38e4b

Please sign in to comment.