Jonáš Fiala

Non-terminating code may be synthesised

2

Given the following example (with `dll` defined as in the examples): ``` { [x, 3] ** x :-> v ** (x + 1) :-> 0 ** (x + 2) :->...

Lift requirement of having the `prusti` feature enabled

9

Having `prusti-contracts = { path = "path/to/prusti-contracts", features = ["prusti"] }` as a dependency breaks regular `cargo build` since the Prusti procedural macros generate `#[prusti::attr = "..."]` attributes and these...

Fixes #529 - [ ] Reorganize `prusti-contracts` workspace

To test either the Free PCS or the Coupling Graph implementation, check out this branch and then use the following commands: To try the FreePCS (owned stuff only) using the...

Start working on the new MicroMir and the PCS analysis for it. Currently everything owned works fully and everything borrows doesn't at all. TODO: - [ ] Add comments to...

TODO: remove existing unwraps

Add option to spawn workers as a module

8

Workers created with the `--target web` flag must be spawned as a module. This adds the option to do that, alleviating the current `--target no-modules` missing features described [here](https://rustwasm.github.io/wasm-bindgen/examples/without-a-bundler.html?highlight=no-modules#using-the-older---target-no-modules). I...

Add method to terminate a worker

5

Adds a `native_worker: RefCell` field to `WorkerBridgeInner` to allow immediately terminating a worker. Since there is no way to tell if a worker has been terminated from a `web_sys::Worker`, uses...

It may not necessarily be possible to break up the computation inside a Worker into nice chunks (e.g. when calling into an external library to do a long-running computation). Thus...

This change: https://github.com/viperproject/silicon/commit/d35ee70d5f64c021e5920f8544fef82768cf2462#diff-384bc38b113bf1202dd85dbd22ddee20345c21ef44a92fdde5fae2abd083ab7fR64-R70 added the `.isFile` and `.canExecute` checks for "z3", but in scala this only checks if `./z3` exists (it is not true that `execute_command(z3Path) doesn't error ==> z3Path.isFile...