Incompleteness of && in overflow checking

[gottschali]

Gobra verifies the following program

package main
func issue(a [10]int, i int) bool {
	return 0 <= i && i < len(a) && a[i] == 0
}

If we check with --overflow we get the error:

Gobra 1.1-SNAPSHOT (@)
(c) Copyright ETH Zurich 2012 - 2024
18:04:47.879 [main] INFO viper.gobra.Gobra - Verifying package /home/ali/eth/thesis/2-memory-access-permission - main [18:04:47]
18:04:51.524 [ForkJoinPool-3-worker-1] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <overflow_incompleteness.go:4:9> Expression may cause integer overflow. 
Index i into a[i] might be negative.

There is no error if we change the && to an if statement and check with --overflow:

func withIf(a [10]int, i int) bool {
	if 0 <= i && i < len(a) {
		return a[i] == 0
	}
	return false
}