Tristan Ravitch
Tristan Ravitch
Right now, a completion can be selected if it is unique. It would be nice to have an ivy-style selector.
There are architecture extensions for: - LLVM/X86 - MC/X86 - MC/PowerPC that are currently not handled in the renderer. These cases need to be filled in.
Currently, there is an `EchoArea` abstraction in the core library. This is meant to represent transient messages like the minibuffer/echo area in emacs. The notion of a transient message makes...
It isn't obvious offhand what is necessary here, but it should be simpler than LLVM
The main goals of the refactor are to: 1. Separate the core memory model data structure from the implementation of primitive crucible support operations (only the former need to be...
This change doesn't compile. This is trying to make the core of the verifier agnostic to the binary format (currently fixed as ELF). This was almost working, except for the...
Inspecting the proof of challenge 3 shows a number of failures that don't have obvious explanations (and seem likely to be false positives). We should fix the easy ones and...
Their tool produces dynamic resolutions of indirect jumps. We should use that to guide code discovery.
We now have support for ARM conditional returns via a macaw architecture-specific extension. We need to add the analogous infrastructure for conditional calls. Contributes to #282
The Weakest Precondition solver had differential summaries. This notion doesn't necessarily translate cleanly to the Strongest Postcondition solver. We still need some way to tell users where divergence in traces...