2016-02-19 11:14:42 +00:00
|
|
|
// +build amd64
|
|
|
|
// errorcheck -0 -d=ssa/prove/debug=3
|
|
|
|
|
|
|
|
package main
|
|
|
|
|
|
|
|
func f0(a []int) int {
|
|
|
|
a[0] = 1
|
2016-03-07 17:36:16 +00:00
|
|
|
a[0] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
a[6] = 1
|
2016-03-07 17:36:16 +00:00
|
|
|
a[6] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
a[5] = 1
|
2016-03-07 17:36:16 +00:00
|
|
|
a[5] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 13
|
|
|
|
}
|
|
|
|
|
|
|
|
func f1(a []int) int {
|
|
|
|
if len(a) <= 5 {
|
|
|
|
return 18
|
|
|
|
}
|
|
|
|
a[0] = 1
|
2016-03-07 17:36:16 +00:00
|
|
|
a[0] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
a[6] = 1
|
2016-03-07 17:36:16 +00:00
|
|
|
a[6] = 1 // ERROR "Proved boolean IsInBounds$"
|
|
|
|
a[5] = 1 // ERROR "Proved non-negative bounds IsInBounds$"
|
|
|
|
a[5] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 26
|
|
|
|
}
|
|
|
|
|
|
|
|
func f2(a []int) int {
|
|
|
|
for i := range a {
|
|
|
|
a[i] = i
|
2016-03-07 17:36:16 +00:00
|
|
|
a[i] = i // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
}
|
|
|
|
return 34
|
|
|
|
}
|
|
|
|
|
|
|
|
func f3(a []uint) int {
|
|
|
|
for i := uint(0); i < uint(len(a)); i++ {
|
|
|
|
a[i] = i // ERROR "Proved IsInBounds$"
|
|
|
|
}
|
|
|
|
return 41
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4a(a, b, c int) int {
|
|
|
|
if a < b {
|
|
|
|
if a == b { // ERROR "Disproved Eq64$"
|
|
|
|
return 47
|
|
|
|
}
|
|
|
|
if a > b { // ERROR "Disproved Greater64$"
|
|
|
|
return 50
|
|
|
|
}
|
2016-03-07 17:36:16 +00:00
|
|
|
if a < b { // ERROR "Proved boolean Less64$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 53
|
|
|
|
}
|
2016-03-07 17:36:16 +00:00
|
|
|
if a == b { // ERROR "Disproved boolean Eq64$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 56
|
|
|
|
}
|
2016-03-07 17:36:16 +00:00
|
|
|
if a > b { // ERROR "Disproved boolean Greater64$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 59
|
|
|
|
}
|
|
|
|
return 61
|
|
|
|
}
|
|
|
|
return 63
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4b(a, b, c int) int {
|
|
|
|
if a <= b {
|
|
|
|
if a >= b {
|
|
|
|
if a == b { // ERROR "Proved Eq64$"
|
|
|
|
return 70
|
|
|
|
}
|
|
|
|
return 75
|
|
|
|
}
|
|
|
|
return 77
|
|
|
|
}
|
|
|
|
return 79
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4c(a, b, c int) int {
|
|
|
|
if a <= b {
|
|
|
|
if a >= b {
|
|
|
|
if a != b { // ERROR "Disproved Neq64$"
|
|
|
|
return 73
|
|
|
|
}
|
|
|
|
return 75
|
|
|
|
}
|
|
|
|
return 77
|
|
|
|
}
|
|
|
|
return 79
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4d(a, b, c int) int {
|
|
|
|
if a < b {
|
|
|
|
if a < c {
|
2016-03-07 17:36:16 +00:00
|
|
|
if a < b { // ERROR "Proved boolean Less64$"
|
|
|
|
if a < c { // ERROR "Proved boolean Less64$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 87
|
|
|
|
}
|
|
|
|
return 89
|
|
|
|
}
|
|
|
|
return 91
|
|
|
|
}
|
|
|
|
return 93
|
|
|
|
}
|
|
|
|
return 95
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4e(a, b, c int) int {
|
|
|
|
if a < b {
|
|
|
|
if b > a { // ERROR "Proved Greater64$"
|
|
|
|
return 101
|
|
|
|
}
|
|
|
|
return 103
|
|
|
|
}
|
|
|
|
return 105
|
|
|
|
}
|
|
|
|
|
|
|
|
func f4f(a, b, c int) int {
|
|
|
|
if a <= b {
|
|
|
|
if b > a {
|
|
|
|
if b == a { // ERROR "Disproved Eq64$"
|
|
|
|
return 112
|
|
|
|
}
|
|
|
|
return 114
|
|
|
|
}
|
|
|
|
if b >= a { // ERROR "Proved Geq64$"
|
|
|
|
if b == a { // ERROR "Proved Eq64$"
|
|
|
|
return 118
|
|
|
|
}
|
|
|
|
return 120
|
|
|
|
}
|
|
|
|
return 122
|
|
|
|
}
|
|
|
|
return 124
|
|
|
|
}
|
|
|
|
|
|
|
|
func f5(a, b uint) int {
|
|
|
|
if a == b {
|
|
|
|
if a <= b { // ERROR "Proved Leq64U$"
|
|
|
|
return 130
|
|
|
|
}
|
|
|
|
return 132
|
|
|
|
}
|
|
|
|
return 134
|
|
|
|
}
|
|
|
|
|
|
|
|
// These comparisons are compile time constants.
|
|
|
|
func f6a(a uint8) int {
|
|
|
|
if a < a { // ERROR "Disproved Less8U$"
|
|
|
|
return 140
|
|
|
|
}
|
|
|
|
return 151
|
|
|
|
}
|
|
|
|
|
|
|
|
func f6b(a uint8) int {
|
|
|
|
if a < a { // ERROR "Disproved Less8U$"
|
|
|
|
return 140
|
|
|
|
}
|
|
|
|
return 151
|
|
|
|
}
|
|
|
|
|
|
|
|
func f6x(a uint8) int {
|
|
|
|
if a > a { // ERROR "Disproved Greater8U$"
|
|
|
|
return 143
|
|
|
|
}
|
|
|
|
return 151
|
|
|
|
}
|
|
|
|
|
|
|
|
func f6d(a uint8) int {
|
|
|
|
if a <= a { // ERROR "Proved Leq8U$"
|
|
|
|
return 146
|
|
|
|
}
|
|
|
|
return 151
|
|
|
|
}
|
|
|
|
|
|
|
|
func f6e(a uint8) int {
|
|
|
|
if a >= a { // ERROR "Proved Geq8U$"
|
|
|
|
return 149
|
|
|
|
}
|
|
|
|
return 151
|
|
|
|
}
|
|
|
|
|
|
|
|
func f7(a []int, b int) int {
|
|
|
|
if b < len(a) {
|
|
|
|
a[b] = 3
|
2016-03-07 17:36:16 +00:00
|
|
|
if b < len(a) { // ERROR "Proved boolean Less64$"
|
|
|
|
a[b] = 5 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
return 161
|
|
|
|
}
|
|
|
|
|
|
|
|
func f8(a, b uint) int {
|
|
|
|
if a == b {
|
|
|
|
return 166
|
|
|
|
}
|
|
|
|
if a > b {
|
|
|
|
return 169
|
|
|
|
}
|
|
|
|
if a < b { // ERROR "Proved Less64U$"
|
|
|
|
return 172
|
|
|
|
}
|
|
|
|
return 174
|
|
|
|
}
|
|
|
|
|
2016-03-07 17:36:16 +00:00
|
|
|
func f9(a, b bool) int {
|
|
|
|
if a {
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
if a || b { // ERROR "Disproved boolean Arg$"
|
|
|
|
return 2
|
|
|
|
}
|
|
|
|
return 3
|
|
|
|
}
|
|
|
|
|
|
|
|
func f10(a string) int {
|
|
|
|
n := len(a)
|
|
|
|
if a[:n>>1] == "aaa" {
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
|
|
|
|
func f11a(a []int, i int) {
|
|
|
|
useInt(a[i])
|
|
|
|
useInt(a[i]) // ERROR "Proved boolean IsInBounds$"
|
|
|
|
}
|
|
|
|
|
|
|
|
func f11b(a []int, i int) {
|
|
|
|
useSlice(a[i:])
|
|
|
|
useSlice(a[i:]) // ERROR "Proved boolean IsSliceInBounds$"
|
|
|
|
}
|
|
|
|
|
|
|
|
func f11c(a []int, i int) {
|
|
|
|
useSlice(a[:i])
|
|
|
|
useSlice(a[:i]) // ERROR "Proved boolean IsSliceInBounds$"
|
|
|
|
}
|
|
|
|
|
|
|
|
func f11d(a []int, i int) {
|
|
|
|
useInt(a[2*i+7])
|
|
|
|
useInt(a[2*i+7])
|
|
|
|
}
|
|
|
|
|
|
|
|
func f12(a []int, b int) {
|
|
|
|
useSlice(a[:b])
|
|
|
|
}
|
|
|
|
|
|
|
|
//go:noinline
|
|
|
|
func useInt(a int) {
|
|
|
|
}
|
|
|
|
|
|
|
|
//go:noinline
|
|
|
|
func useSlice(a []int) {
|
|
|
|
}
|
|
|
|
|
2016-02-19 11:14:42 +00:00
|
|
|
func main() {
|
|
|
|
}
|