stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
Make sure that, when we import StaticChecks, all specification constructs: - result in a no-op, without crashes or side effects - have only constant overhead (e.g. due to closure creation),...
GenC partially evaluates certain initialization patterns, possibly due to Array.fill forcing side effects. We should support more initialization patterns to ensure that both arrays are initialized (even when they are...
This PR adds let-bindings in favor of duplicating code in two more places (match desugaring and assertions for ADT field selections). Conversely, it also adds an additional let-simplifications step in...
## 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...
The following goes through: ```scala import stainless._ import stainless.lang._ import stainless.annotation._ object DecreasesNotDecreasing { @opaque def f(x: BigInt): Unit = { decreases(x) require(x >= 0) f(x + 1) }.ensuring(_ =>...
For instance, the following snippet: ```scala import stainless.annotation._ object GenCTest { case class Box(value: Int) @cCode.`export` def test: Unit = { val boxes = Array.fill(10)(Box(123)) } } ``` gets essentially...
Imlement [basic `parallel` construct library](https://www.youtube.com/watch?v=KkMZGJ3M2-o) that works for both Scala on JVM and genc. For `genc`, the implementation could use pthreads : https://www.cs.cmu.edu/afs/cs/academic/class/15492-f07/www/pthreads.html
Scala already has implementation for `require` and `ensuring`, but not for `decreases`. We can implement run-time check for a generalization of decreases as sketched in the attached file for a...
Investigate if it is feasible to peroform tail recursion elimination in genc itself, for non-mutual recursion. Currently, this is not needed when using genc with GCC output, which performs tail...
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...
