stainless

stainless copied to clipboard

For `@synthetic` functions we re-assert postconditions at inlined call sites (see https://github.com/epfl-lara/stainless/blob/3da44e47828dd6269131270b76ada1617eb00b6a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala#L114). The particular way in which this is done, i.e., by let-binding the post condition and *then* asserting the...

gsps

Put "fat" JAR on a diet?

2

This is a low-priority feature request. GitHub limits individual file sizes by default to 100MB. Because we commit the fat JAR to our GitHub repo (yes, I know...), its size...

sfiruch

String support?

3

It seems string operations are unsupported `object asdf { def testString(s: String):Boolean = s.isEmpty }` Stainless error: stainless.frontend.package$UnsupportedCodeException: Unknown call to isEmpty on s (String) with arguments List() of type...

mwookawa

Mutable fields in traits cannot have a default value when using var inside @extern class

2

This code: ```scala @extern case class Foo() { var counter: Int = 0 } ``` shows message: ``` [ Error ] extern.scala:5:5: Mutable fields in traits cannot have a default...

vkuncak

The combination of - using a type class, - having a recursive data type and - matching on a `Tuple2` ADT makes Stainless time out on the following benchmark: ```scala...

yannbolliger

Problem proving lemma with imperative features

1

Thanks to Romain (J) for reporting Stainless times out on the assertion `arePositive(l)`. ```scala import stainless.collection._ object Imperative { case class Test(var l: List[BigInt]) { def lemma(x: BigInt, amount: BigInt)...

jad-hamza

Replace VC cache backend with embedded database

3

romac

Support for breakable and break (Was: Missing dependencies for breakable, break)

4

Ok this one is a Sev 2 from my vantage point. Stainless does not support `return`. One way out -- when attempting to get existing (Scala) code to work with...

saraswat

@inlineOnce on recursive functions

3

Since I've enabled inlining (once) of recursive functions in themselves, this example fails: ```scala import stainless.annotation._ import stainless.collection._ import stainless.lang._ object InlineOnce { def test(l: List[BigInt]): Unit = { require(arePositive(l)...

jad-hamza

Better support for proving method equivalence

1

The easiest to explain form of strong specification is having two versions of a method and proving that one behaves just like the other (possibly under some joint precondition). The...

vkuncak