From 3d7ced7f969c1bdc57ee3105184ff7cc3eb57fe6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 31 Oct 2023 12:36:12 -0400 Subject: [PATCH] crucible-llvm-syntax: README --- crucible-llvm-syntax/README.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 crucible-llvm-syntax/README.md diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md new file mode 100644 index 000000000..49f3c95ee --- /dev/null +++ b/crucible-llvm-syntax/README.md @@ -0,0 +1,16 @@ +# crucible-llvm-syntax + +This package provides concrete syntax for Crucible-LLVM types and operations. + +Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn]. +This `ParserHooks` supports the following types and statements: + +**Types**: + +- `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide. For example `(Ptr 8)` is the type of bytes. + +**Statements**: + +- `null : Ptr n` is the null pointer, i.e. the pointer with both block number and offset concretely set to zero. The width of the null pointer is determined by the `?ptrWidth` implicit parameter used when constructing the `ParserHooks` + +[syn]: ../crucible-syntax