stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
Given the realistic concern of bugs in the transpiler, we should consider generating C code whose at least memory safety can be checked independently, using, for example, Frama-C: https://frama-c.com/html/documentation.html
Consider the following snippet: ```scala object TargetMutatedCondition { case class Box(var value: Int) def test: Unit = { val b1 = Box(123) val b2 = Box(456) val b3 = if...
We should perform such checks because the following snippet results in a C code exhibiting UB: ```scala import stainless.io._ import stainless.lang._ import stainless.annotation._ object GenCArrayFieldReplaceVLA { @cCode.noMangling case class Buffer(var...
Similar to #1286 but involves arrays: ```scala import stainless.io._ import stainless.lang._ import stainless.annotation._ object Scratch { @cCode.noMangling case class Box(var value: Int, extra: Int) @cCode.`export` def main(): Int = {...
Similar to https://github.com/epfl-lara/stainless/issues/1284, the following snippet is incorrectly translated: ```scala import stainless.proof._ import stainless.io._ import stainless.lang._ import stainless.annotation._ object GenCRefCopy2 { @cCode.noMangling case class Ref(var x: Int, var y: Int)...
The `replace` function of the following snippet is not correctly translated: ```scala import stainless.io._ import stainless.lang._ import stainless.annotation._ object GenCArrayFieldReplace { @cCode.noMangling case class Buffer(var array: Array[Int], extra: Int) {...
One can "hide" arrays through class hierarchy/ADTs, as in the following snippet: ```scala import stainless._ import stainless.lang._ import stainless.io._ import stainless.annotation._ object GenCReturnArray { @cCode.noMangling sealed trait OptionArray @cCode.noMangling case...
The following snippet illustrates the problem: ```scala import stainless.proof._ import stainless.io._ import stainless.lang._ import stainless.annotation._ object GenCRefCopy { case class Ref(var x: Int, var y: Int) def id(r: Ref): Ref...
The following snippet causes a crash in GenC: ```scala import stainless._ import stainless.lang._ import stainless.annotation._ import StaticChecks._ object LZWDecls { @inline @cCode.inline val DictionarySize = 6 @inline @cCode.inline val BufferSize...
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],...
