2016-02-19 11:14:42 +00:00
|
|
|
// +build amd64
|
2016-10-19 15:47:52 +00:00
|
|
|
// errorcheck -0 -d=ssa/prove/debug=1
|
2016-02-19 11:14:42 +00:00
|
|
|
|
2016-04-12 16:24:34 +00:00
|
|
|
// Copyright 2016 The Go Authors. All rights reserved.
|
|
|
|
// Use of this source code is governed by a BSD-style
|
|
|
|
// license that can be found in the LICENSE file.
|
|
|
|
|
2016-02-19 11:14:42 +00:00
|
|
|
package main
|
|
|
|
|
2016-03-23 17:20:44 +00:00
|
|
|
import "math"
|
|
|
|
|
2016-02-19 11:14:42 +00:00
|
|
|
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-03-23 17:20:44 +00:00
|
|
|
a[5] = 1 // ERROR "Proved IsInBounds$"
|
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
|
|
|
|
}
|
2016-03-23 17:20:44 +00:00
|
|
|
a[0] = 1 // ERROR "Proved non-negative bounds IsInBounds$"
|
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-03-23 17:20:44 +00:00
|
|
|
a[5] = 1 // ERROR "Proved IsInBounds$"
|
2016-03-07 17:36:16 +00:00
|
|
|
a[5] = 1 // ERROR "Proved boolean IsInBounds$"
|
2016-02-19 11:14:42 +00:00
|
|
|
return 26
|
|
|
|
}
|
|
|
|
|
2016-03-23 17:20:44 +00:00
|
|
|
func f1b(a []int, i int, j uint) int {
|
2016-04-02 08:29:11 +00:00
|
|
|
if i >= 0 && i < len(a) {
|
|
|
|
return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
|
|
|
|
}
|
|
|
|
if i >= 10 && i < len(a) {
|
|
|
|
return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
|
|
|
|
}
|
|
|
|
if i >= 10 && i < len(a) {
|
|
|
|
return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
|
|
|
|
}
|
|
|
|
if i >= 10 && i < len(a) { // todo: handle this case
|
|
|
|
return a[i-10]
|
2016-03-23 17:20:44 +00:00
|
|
|
}
|
|
|
|
if j < uint(len(a)) {
|
2016-04-02 08:29:11 +00:00
|
|
|
return a[j] // ERROR "Proved IsInBounds$"
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f1c(a []int, i int64) int {
|
|
|
|
c := uint64(math.MaxInt64 + 10) // overflows int
|
|
|
|
d := int64(c)
|
|
|
|
if i >= d && i < int64(len(a)) {
|
|
|
|
// d overflows, should not be handled.
|
|
|
|
return a[i]
|
2016-03-23 17:20:44 +00:00
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
2016-02-19 11:14:42 +00:00
|
|
|
func f2(a []int) int {
|
|
|
|
for i := range a {
|
2016-03-02 11:58:27 +00:00
|
|
|
a[i+1] = i
|
|
|
|
a[i+1] = 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)
|
2016-06-25 20:40:43 +00:00
|
|
|
if a[:n>>1] == "aaaaaaaaaaaaaa" {
|
2016-03-07 17:36:16 +00:00
|
|
|
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])
|
|
|
|
}
|
|
|
|
|
2016-03-23 17:20:44 +00:00
|
|
|
func f13a(a, b, c int, x bool) int {
|
|
|
|
if a > 12 {
|
|
|
|
if x {
|
|
|
|
if a < 12 { // ERROR "Disproved Less64$"
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a <= 12 { // ERROR "Disproved Leq64$"
|
|
|
|
return 2
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a == 12 { // ERROR "Disproved Eq64$"
|
|
|
|
return 3
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a >= 12 { // ERROR "Proved Geq64$"
|
|
|
|
return 4
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a > 12 { // ERROR "Proved boolean Greater64$"
|
|
|
|
return 5
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 6
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13b(a int, x bool) int {
|
|
|
|
if a == -9 {
|
|
|
|
if x {
|
|
|
|
if a < -9 { // ERROR "Disproved Less64$"
|
|
|
|
return 7
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a <= -9 { // ERROR "Proved Leq64$"
|
|
|
|
return 8
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a == -9 { // ERROR "Proved boolean Eq64$"
|
|
|
|
return 9
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a >= -9 { // ERROR "Proved Geq64$"
|
|
|
|
return 10
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a > -9 { // ERROR "Disproved Greater64$"
|
|
|
|
return 11
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 12
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13c(a int, x bool) int {
|
|
|
|
if a < 90 {
|
|
|
|
if x {
|
|
|
|
if a < 90 { // ERROR "Proved boolean Less64$"
|
|
|
|
return 13
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a <= 90 { // ERROR "Proved Leq64$"
|
|
|
|
return 14
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a == 90 { // ERROR "Disproved Eq64$"
|
|
|
|
return 15
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a >= 90 { // ERROR "Disproved Geq64$"
|
|
|
|
return 16
|
|
|
|
}
|
|
|
|
}
|
|
|
|
if x {
|
|
|
|
if a > 90 { // ERROR "Disproved Greater64$"
|
|
|
|
return 17
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 18
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13d(a int) int {
|
|
|
|
if a < 5 {
|
|
|
|
if a < 9 { // ERROR "Proved Less64$"
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13e(a int) int {
|
|
|
|
if a > 9 {
|
|
|
|
if a > 5 { // ERROR "Proved Greater64$"
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13f(a int64) int64 {
|
|
|
|
if a > math.MaxInt64 {
|
|
|
|
// Unreachable, but prove doesn't know that.
|
|
|
|
if a == 0 {
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13g(a int) int {
|
|
|
|
if a < 3 {
|
|
|
|
return 5
|
|
|
|
}
|
|
|
|
if a > 3 {
|
|
|
|
return 6
|
|
|
|
}
|
|
|
|
if a == 3 { // ERROR "Proved Eq64$"
|
|
|
|
return 7
|
|
|
|
}
|
|
|
|
return 8
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13h(a int) int {
|
|
|
|
if a < 3 {
|
|
|
|
if a > 1 {
|
|
|
|
if a == 2 { // ERROR "Proved Eq64$"
|
|
|
|
return 5
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return 0
|
|
|
|
}
|
|
|
|
|
|
|
|
func f13i(a uint) int {
|
|
|
|
if a == 0 {
|
|
|
|
return 1
|
|
|
|
}
|
|
|
|
if a > 0 { // ERROR "Proved Greater64U$"
|
|
|
|
return 2
|
|
|
|
}
|
|
|
|
return 3
|
|
|
|
}
|
|
|
|
|
2016-03-07 17:36:16 +00:00
|
|
|
//go:noinline
|
|
|
|
func useInt(a int) {
|
|
|
|
}
|
|
|
|
|
|
|
|
//go:noinline
|
|
|
|
func useSlice(a []int) {
|
|
|
|
}
|
|
|
|
|
2016-02-19 11:14:42 +00:00
|
|
|
func main() {
|
|
|
|
}
|