Romain Ruetschi

Add clippy to Travis and remove unnecessary code

5

On hold. See https://github.com/SpinResearch/RustySecrets/pull/66#issuecomment-391170134.

https://github.com/japaric/criterion.rs

https://github.com/rust-unofficial/awesome-rust/

https://github.com/japaric/trust

WebAssembly backend

1

## reclang IR Defines a language, 'reclang', that functions as an intermediate language between stainless trees and wasm code. The main feature of reclang is that its structured types are...

Remote verification server

3

Let's investigate what a remote verification server would look like. 1. Set up a container-based Inox server with a shared verification cache 2. Add a `--remote-server=URL` flag to Stainless to...

Fix model checking of inlined ADT invariant

4

Running Stainless on this benchmark: ```scala import stainless.lang._ import stainless.annotation._ object inlineInv { @inlineInvariant sealed abstract class Toto case class Foo(x: BigInt) extends Toto { require(x > 10) } def...

~~Blocked by https://github.com/epfl-lara/inox/pull/111~~

Ghost checker should disallow pattern matching on a ghost field

3

```scala import stainless.lang._ import stainless.annotation._ object GhostMatch { case class Foo(@ghost value: Option[BigInt]) def nonGhostMatch(foo: Foo) = { foo match { // should fail because foo.value will not exist at...