Ted Kaminski
Ted Kaminski
There are some docker files that already exist for testing the Kani install procedure on different OSes that might serve as a starting point. For instance here is the ubuntu-latest...
Do you have a specific goal here? Or just trying things out? Just curious. It's really hard to accurately model many numerical functions. It might be feasible to get it...
1. We should revisit the limitations section for sure, even if to make sure it's accurate to our current capabilities... 2. This is a good point about "what theory." We'd...
BTW I'd add the same flags as `cargo build` So `--workspace` and `--all-features` looks like
Probably a bug on our side, I did a quick test with cbmc: ``` ** Results: test.c function main [main.unwind.0] line 3 unwinding assertion loop 0: FAILURE ```
Some quick analysis of the cause: A `cargo install` invocation shares one "global" `CompileOptions`, which always has `spec = Packages::Default`. (This is just because `cargo install` doesn't take any of...
After a bit more investigation, I think this issue is narrower than I originally thought. `cargo install` effectively does a `cargo build --release` in the requested package. For most packages,...
> Can you please clarify what you plans are? I can't tell from this PR how you are planning to parallelize each execution. This PR just takes the two places...
> I am assuming you want one runner per harness, don't you? Nope, it's about running them all. Really the only major need for this object is that the runner...
> Ideally, we'd probably want an `async run_harness()` function to allow easy parallelization. Indeed! Threads are a simpler starting point, however. (Besides dependencies, there's also a problem of _limiting concurrency_....