stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
In this example, the VC for the precondition check in the call to `gg` in the `insert` function takes ~2 minutes to solve. It's probably `z3` (tried with 4.8.6 and...
Running the example from https://github.com/epfl-lara/stainless/issues/979 in portfolio mode with `--vc-cache=false --solvers=smt-z3,smt-cvc4 --timeout=N` takes around `N` seconds (+loading) and succeeds with the (body assertion) VC being verified in exactly `N` seconds....
I tried to encode a simple directed graph library and crashed stainless with this error: https://github.com/NicolasRouquette/stainless-bundle-closure/tree/10366df0c54395dd99bacb9451256c625d3ef5cc#v4-commit This is with Stainless 0.7.4, sbt 1.3.0, scala 2.12.9 running on ubuntu 20.04 ```...
https://github.com/epfl-lara/stainless/blob/391088ee6ea1154db23e1320d8f637b350c593c0/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala#L162-L180 See discussion: https://github.com/epfl-lara/stainless/pull/985#discussion_r614204561
cc: @deiruch This makes IDEs who count 1 tab = 1 column misreport positions of warnings and errors. We could adjust positions down by fetching the source code line and...
The following code fragment does not validate. ``` import stainless.math.BitVectors._ import scala.language.postfixOps object Constants { val CONSTANT = 4096 * 64 } case class Test() { def x(x: UInt32): Unit...
This is an example that seems to be solved by Z3 in non-incremental mode, but times out with incremental mode. We can add it to the test suite if we...
Not really a Stainless issue, but we can leave this open until this works better in Z3. This example generates a VC for the assertion, which is hard to solve...
After updating the rust-interop branch from 533f5d5 to 20d258d (#936), we encountered some failing behaviour in the MeasureInference phase. The following example in Rust suddenly loops infinitely, after the update....
This is a problem when running Stainless on Windows in watch-mode. It appears that Stainless might keep file handles open for longer than strictly necessary. This is problematic, as files...