Federico Poli
Federico Poli
Currently, `rustup` needs to be in the `PATH` used by VS Code. This is not flexible enough for some use cases. See the comment [here](https://github.com/viperproject/prusti-assistant/issues/35#issuecomment-1896398749). For improved flexibility, we could...
As described in the readme, the extension currently requires ~~Java >=12~~ Java >=11 and Rustup >=1.23. It would be useful to check these versions at startup, as part of the...
The Viper IDE took its `spawn` function from this repository. In the process, they did some nice changes, among with a check of the exist code of the spawned process:...
Currently there is no easy way of sending configuration flags to the Prusti server. It would be useful to allow that, to enable for example the `DUMP_VIPER_PROGRAM` flag that dumps...
When a user tries to run a command like `prusti-assistant.verify` before the extension has been fully initialized, nothing happens and no error message is shown. This is confusing for the...
Jonas made me realize that this optimization (used by Prusti) is wrong when `left < 0`, because in Viper `-3 / 2 == -2` but in Scala (and Rust) `-3...
The [Scalastyle](http://www.scalastyle.org/) linter complains about missing `hashCode` definitions in Silver. I'm not sure if we did that intentionally but it seems worth double-checking, adding a comment to Silver if there...
With Z3 it's possible to [declare special relations](https://microsoft.github.io/z3guide/docs/theories/Special%20Relations) such as partial order, linear order, etc. The documentation explains that the decision procedure is efficient and avoids the quadratic number of...
By profiling for 165 seconds a Carbon run with VisualVM I found that: * The time spent in the JVM is 53s, which is 32% of the wall-clock time. *...
The AST of a program containing a top-level function with a quote (`'`) in its name passes the consistency checks. However, the dump of the program is rejected by the...