robdockins
robdockins
The following interaction demonstrates that TernayTrie does not always maintain its structural invariant. I have not yet tracked down the cause. It may be a bug in the statement of...
Would it be easy to add support for the `:global-declarations` option and the `get-info` operation? They are convenient for certain kinds of interactive use cases. Cf http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf ``` $ stp...
Minor enhancements to the code generation process. This adds volatile qualifiers to external stream global variables, and allows users to select an output directory for generated code.
The generated C code takes some care to copy the values of all the "external" streams from shared global variables to private globals before beginning the remainder of its work....
The `local` combinator is intended to act like an internal `let` operation, but doesn't seem to be handled correctly. In particular, if a stream bound via `local` is passed into...
Looking at the datatypes involved in the high-level and low-level `Spec` datatypes (e.g. `SpecItem`), it seems to me that properties and theorems are both represented as a bare stream of...
While running some routine tests, QC uncovered what appears to be an error. I haven't investigated yet, but here's the QC output. ``` BLT: running QuickCheck tests ... *** Failed!...
I am experimenting with this package and cannot use `withTaskGroup` for my setting (because I'm in a custom monad). I can reimplement most of it from the outside, except that...
It seems that this aspect of the data layout string was removed starting with LLVM 3.5.0. As best I can tell, we only support LLVM back to the 3.5 series,...
Right now, the only information tracked in the strongest-postcondition verifier is the "binary" relational information that indicates what values are (in)equivalent between the two binaries. We also need to track...