Skip to content

Don't load slice values in a for range unless they're explicitly used in the for statement #600

@upamanyus

Description

@upamanyus

This has a data race:

package main

func main() {
	sl := make([]string, 1)
	go func () {
		var x string
		_ = x
		for _, x = range sl {
		}
	}()
	sl[0] = ""
}

but changing the for loop to for _, _ = range sl { fixes it. Currently, Goose models both as a data race, because the same slice.for_range iterator is used, which requires loading the value of each element. This is a conservative semantics, but makes some programs difficult/impossible to prove (e.g. this is more annoying than necessary https://github.com/goose-lang/goose/blob/c12b8af04edef8ccdee729bbd0149f5161531987/testdata/examples/channel/workq/w.go#L75-L77)

(Copied from goose-lang/goose#188.)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions