|
|
|---|
|
|
|
|---|
Parsing for our C syntax for tools.
We provide an executable parser from the concrete syntax to the abstract syntax. The parser is fairly efficient by way of using a stobj.
Currently the parser is neither verified nor proof-generating, but we plan to work towards these goals.