João Pereira
João Pereira
(Draft PR; I will revisit this in the future. This change may be useful if we want in the future to limit the automation that we currently have for the...
Recent versions of z3 (`4.8.9` and beyond) have introduced changes to the possible outputs of z3 ([issue](https://github.com/Z3Prover/z3/issues/4425), [commit 1](https://github.com/Z3Prover/z3/commit/9f8887cc2ef8248aaeb01b5afe3507923f364b4e), [commit 2](https://github.com/Z3Prover/z3/commit/80d5d661589e6283b5df3a8fd34f2c1eaad7f353)). Silicon does not seem to be prepared to handle...
We are not taking into account that the order of evaluation of the components of composite literals is pretty much undefined, apart from function calls, as mentioned [here](https://golang.org/ref/spec#Order_of_evaluation). Taking an...
## Shared variables Whenever we have an assignment of the form ```go x@ := expr // of type T ``` Gobra translates this as following (internal representation) ``` init x...
In Scion, I have a program of the following form: ```go func (d *DataPlane) Run() { read /*@@@*/ := // spec hidden func /*@ rc @*/ (ingressID uint16, rd BatchConn)...
TODO: elaborate ```go package p type scmpError struct { TypeCode int Cause error } preserves e.ErrorMem() ensures e.Size() == old(e.Size()) decreases e.Size() func (e scmpError) Error() string /*{ unfold e.ErrorMem()...
Currently, Gobra produces an error message when one tries to call a closure stored in a field as in the following program: ```go package main type T struct { f...
In Go, the following snippet causes an error at compile time ```go package main const A = 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000992 func s(i int) {} func main() { s(A) } ``` Error: ```...