antonis19
antonis19
In the program below, because of the line where the channel is closed the following happen: i) GMC synthesis fails. ii) The global graph constructed ends up being simpler than...
Dingo-Hunter is not able to detect a deadlock for the program below: (you can also find the code in this pastebin link https://pastebin.com/C4Md3yLB). The extracted CFSMs are correct, however the...
Actions after an internal choice or after an external choice (select-case) are assigned to one branch of each choice. (so there is no merge point after the choice). For example,...
The following program will generate unparsable MiGo types because of importing the ```net``` package. Moreover, the generated ```os.NewFile#``` functions degenerate to an empty channel operation (```tau```). ```go package main import...
The MiGo types extracted for this program [twobuyers.go](https://pastebin.com/TQPYp8tR) have an issue. For the buyer1 goroutine migoinfer gets the order and type of operations right, but the operations are presented as...
In the program [examplewithstruct.go](https://pastebin.com/KyTw7tbA) the channels are encapsulated in a struct which is passed as a pointer to the two goroutines. endChannel is used to signal to main that a...
This PR avoids the nil panic in the special case when the changeset is empty during unwinding.
Adds a command to read branch data from latest commitment domain. Usage: `go run cmd/read-branch/main.go --datadir /path/to/datadir --prefix 0a1b`
# Rationale Today's zkVMs rely on execution witnesses as inputs to their provers. This is now mostly happening using Reth's `debug_executionWitness` RPC endpoint. With Reth however, this only works well...