Jad Hamza

Equations generates an unexpected obligation, and admitting it makes an anomaly

1

Hello, This example of Equations (master version with Coq master from 06/10/2019) on `f` generates an obligation that refers to `f_graph` and that is not proved automatically. Morever, admitting this...

Hello, On version Coq/Equations master (06/10/2019), I'm getting this error on the following code: ```coq Require Import Coq.Lists.List. Import ListNotations. Require Import Equations.Equations. Equations unit_type (l: list nat) (pre: ~(l...

Incorrect universe constraints declared for inductive type

3

This program is similar to #240, except that I have replaced `T2` with `nat`. I get a different error, so I'm not sure if this is the same bug (feel...

Type error after type encoding with Nil()

3

A type error happens after the type encoding phase on this example. (Workaround: write `Nil[T]()` instead of `Nil()`). ```scala import stainless.collection._ import stainless.annotation._ object TypeEncodingNil { @extern def f[T](l: List[T],...

Classes with multiple parameter groups

3

This is currently not supported by Stainless: ```scala case class C(var x: Int)(var y: Int = x) { } ``` ``` Variables are only allowed within functions and as constructor...

Function equivalence with comparefuns crashes

3

Hi @drganam @vkuncak, can Stainless generate equivalence lemmas for functions when one of the function calls other functions? (here `replace` vs `slowReplace`). I get a crash on this example (from...

Write Scala implementation for BitVectors library

1

https://github.com/epfl-lara/stainless/blob/aa48894c6e4bf4b3eec7e9f3f26d76754c4d0f63/frontends/library/stainless/math/BitVectors.scala#L10

Stainless Actors

5

Since we've added checks to arguments aliasing https://github.com/epfl-lara/stainless/pull/965, the stainless actors fails because of aliasing here: https://github.com/epfl-lara/stainless-actors/blob/8173788e75880fa04d004cd8443ed0ef70b1cd83/examples/kvs/src/main/scala/KVS.scala#L67 There is aliasing between `ctx.self` and the implicit parameter `ctx` being passed to...

Unsoundness with quantifiers (choose nothing and always succeed)

3

I don't remember why this example with `assert(false)` is in the valid benchmarks? https://github.com/epfl-lara/stainless/blob/5b7b3a0c01c23486fea44abb2255f0963a242708/frontends/benchmarks/verification/valid/Countable2.scala This should be rejected? (probably the assertion line 33) Also quantifiers for the type-checker should probably...

Error with type members: Cannot apply ClassFieldAccessor to type thiss.T

1

Example `TypeMembers2.scala` which was in `extraction/valid` (was temporarily removed in #1088) crashes: ```scala import stainless.annotation._ object TypeMembers2 { abstract class M { @mutable type T def c(t: T): Unit }...