Samuel Chassot
Samuel Chassot
Hi everyone, hi @tahina-pro, I read the papers and am interested in the parser/serialiser pair generation of everparse. In the README.md it is also mentioned that this project is about...
As I had to figure out how to use `quackyducky` during my research, I thought I could contribute to the documentation with what was missing. I would be happy to...
Hi! I am trying to test everparse and, as I am working on MacOS and am not expecting to modify the code, I am trying to use the Docker image....
Stainless verifies this program: ``` import stainless.lang._ import stainless.collection._ import stainless.annotation._ case class X(var x: BigInt) object Unsound: def simplerUnsoundExample(): Unit = { val a = Array[X](X(0), X(0), X(0)) val...
when working with laws in trait, for example: ``` sealed trait Serialiser[T]: def serialise(x: T): List[Char] def deserialise(l: List[Char]): Option[T] @law def serialiseDeserialise(x: T): Boolean = deserialise(serialise(x)) == x end...
Add `computes` that works as follows: ``` def f(x: BigInt): BigInt = { body(x) } computes(v(x)) ``` By default, `computes` behaves as `ensuring(_ == v(x))` but with `StaticChecks`, it inlines...
When using this feature unavailable of CVC4/5, an error message is displayed even though the VC is verified by another available solver. This could be a message displayed only in...
CVC4 is not available on arm64 architecture so I built it from source. For the build process to go through, I had to make some modifications to a file of...
It would be interesting to have access, as a developer, to the measures Stainless infers. In some cases, we would like to add them explicitly but, if Stainless can infer...