nicolasdilley / Gomela

Tool developped for "Bounded verification of message passing concurrency in Go programs."
39 stars 7 forks source link

DeferStmt doesnt behave as expected. #6

Open nicolasdilley opened 3 years ago

nicolasdilley commented 3 years ago

At the moment they are always printed at the end of the blockstmt. However, in the case of a return, they are bypassed

go func() { defer func() { <-limitCh }() defer wg.Done()

        path, version, agent, ok, err := isGo(pr)
        if err != nil {
            // TODO(jbd): Return a list of errors.
        }
        if !ok {
            return
        }
        found <-0
    }()

for example in this case, the return will bypass the deferstmts. One solution is to add the deferstmts at the end of the body of the proctype being generated.