stainless

stainless copied to clipboard

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...

jad-hamza

In principle, the principles are simple. In practice...

vkuncak

Ghost code analysis should be improved (e.g. copying ADT constructor with a ghost field seems to fail). But then, it should be documented. We should explore its use for history...

vkuncak

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 }...

jad-hamza

This is currently not working with stainless: ``` something match { case A | B => FooBar(a,b) } ``` instead you have to write: ``` something match { case A...

fschramka

Unapply with a subclass as argument is incorrectly handled

1

Here is the minimised code: ```scala import stainless.lang._ abstract sealed class Top() case class Nil() extends Top() case class Pair(t1: Top, t2: Top) extends Top() object Alias1{ def unapply(t: Top):...

Sporarum

Add shallow equality to the full-imperative pipeline

4

This PR adds up to the PR #862 and adds the following: - *Shallow equality*: a new type of equality, denoted by `=~` (and `!=~` for its negation, though that...

brunnerant

Crash in compileLambda in CodeGeneration

8

This files (a minimized version of `GodelNumbering`) crashes on the assertion here: https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/core/src/main/scala/stainless/codegen/CodeGeneration.scala#L355 ``` stainless Test.scala --solvers=smt-z3 --batched --vc-cache=false --codegen --debug=stack --feeling-lucky ``` ```scala import stainless.lang._ import stainless.equations._ import stainless.annotation._...

jad-hamza

Not enough checks for initialization soundness

7

```scala object Test { case class B(val x: Int) sealed abstract class Top { val g: B = this.foo val h: B = B(2) def foo = { B(3) }...

vkuncak

Equality is not the dispatched equality in Stainless

2

Stainless interprets == as the logical equality, which is not consistent with Scala in case equality is overridden with relations that do not satisfy congruence properties. The Stainless interpreter is...

vkuncak