Stowage/go
2
0
Fork 0
mirror of https://github.com/golang/go.git synced 2025-12-08 06:10:04 +00:00
Code Issues Projects Releases Packages Wiki Activity

test: go fmt prove.go tests

Browse source 
Change-Id: Ia4c2ceffcf2bfde862e9dba02a4b38245f868692
Reviewed-on: https://go-review.googlesource.com/c/go/+/721202
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Sean Liao <sean@liao.dev>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Mark Freeman <markfreeman@google.com>
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
This commit is contained in:
Jorropo 2025-11-18 00:54:38 +01:00 • committed by Gopher Robot
parent 489d3dafb7
commit 2239520d1c
1 changed files with 39 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

79
test/prove.go
View file

@ -991,14 +991,14 @@ func divShiftClean64(n int64) int64 {
if n < 0 { if n < 0 {
return n return n
} }
return n / int64(16) // ERROR "Proved Div64 is unsigned$" return n / int64(16) // ERROR "Proved Div64 is unsigned$"
} }
func divShiftClean32(n int32) int32 { func divShiftClean32(n int32) int32 {
if n < 0 { if n < 0 {
return n return n
} }
return n / int32(16) // ERROR "Proved Div32 is unsigned$" return n / int32(16) // ERROR "Proved Div32 is unsigned$"
} }
// Bounds check elimination // Bounds check elimination
@ -1079,8 +1079,8 @@ func modu2(x, y uint) int {
func issue57077(s []int) (left, right []int) { func issue57077(s []int) (left, right []int) {
middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$" middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$"
left = s[:middle] // ERROR "Proved IsSliceInBounds$" left = s[:middle] // ERROR "Proved IsSliceInBounds$"
right = s[middle:] // ERROR "Proved IsSliceInBounds$" right = s[middle:] // ERROR "Proved IsSliceInBounds$"
return return
} }
@ -2496,7 +2496,6 @@ func div3pos(x []int) int {
return len(x) / 3 // ERROR "Proved Div64 is unsigned" return len(x) / 3 // ERROR "Proved Div64 is unsigned"
} }
var len200 [200]int var len200 [200]int
func modbound1(u uint64) int { func modbound1(u uint64) int {
@ -2544,9 +2543,9 @@ func rangebound2(x []int) int {
func swapbound(v []int) { func swapbound(v []int) {
for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable" for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
v[i], // ERROR "Proved IsInBounds" v[i], // ERROR "Proved IsInBounds"
v[len(v)-1-i] = // ERROR "Proved IsInBounds" v[len(v)-1-i] = // ERROR "Proved IsInBounds"
v[len(v)-1-i], v[len(v)-1-i],
v[i] // ERROR "Proved IsInBounds" v[i] // ERROR "Proved IsInBounds"
} }
} }
@ -2569,73 +2568,73 @@ func rightShiftBounds(v, s int) {
// We care about the bounds for x printed on the prove(x) lines. // We care about the bounds for x printed on the prove(x) lines.
if -8 <= v && v <= -2 && 1 <= s && s <= 3 { if -8 <= v && v <= -2 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-4,-1 " prove(x) // ERROR "Proved sm,SM=-4,-1 "
} }
if -80 <= v && v <= -20 && 1 <= s && s <= 3 { if -80 <= v && v <= -20 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-40,-3 " prove(x) // ERROR "Proved sm,SM=-40,-3 "
} }
if -8 <= v && v <= 10 && 1 <= s && s <= 3 { if -8 <= v && v <= 10 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-4,5 " prove(x) // ERROR "Proved sm,SM=-4,5 "
} }
if 2 <= v && v <= 10 && 1 <= s && s <= 3 { if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=0,5 " prove(x) // ERROR "Proved sm,SM=0,5 "
} }
if -8 <= v && v <= -2 && 0 <= s && s <= 3 { if -8 <= v && v <= -2 && 0 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-8,-1 " prove(x) // ERROR "Proved sm,SM=-8,-1 "
} }
if -80 <= v && v <= -20 && 0 <= s && s <= 3 { if -80 <= v && v <= -20 && 0 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-80,-3 " prove(x) // ERROR "Proved sm,SM=-80,-3 "
} }
if -8 <= v && v <= 10 && 0 <= s && s <= 3 { if -8 <= v && v <= 10 && 0 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-8,10 " prove(x) // ERROR "Proved sm,SM=-8,10 "
} }
if 2 <= v && v <= 10 && 0 <= s && s <= 3 { if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=0,10 " prove(x) // ERROR "Proved sm,SM=0,10 "
} }
if -8 <= v && v <= -2 && -1 <= s && s <= 3 { if -8 <= v && v <= -2 && -1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-8,-1 " prove(x) // ERROR "Proved sm,SM=-8,-1 "
} }
if -80 <= v && v <= -20 && -1 <= s && s <= 3 { if -80 <= v && v <= -20 && -1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-80,-3 " prove(x) // ERROR "Proved sm,SM=-80,-3 "
} }
if -8 <= v && v <= 10 && -1 <= s && s <= 3 { if -8 <= v && v <= 10 && -1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=-8,10 " prove(x) // ERROR "Proved sm,SM=-8,10 "
} }
if 2 <= v && v <= 10 && -1 <= s && s <= 3 { if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
prove(x) // ERROR "Proved sm,SM=0,10 " prove(x) // ERROR "Proved sm,SM=0,10 "
} }
} }
func unsignedRightShiftBounds(v uint, s int) { func unsignedRightShiftBounds(v uint, s int) {
if 2 <= v && v <= 10 && -1 <= s && s <= 3 { if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
proveu(x) // ERROR "Proved sm,SM=0,10 " proveu(x) // ERROR "Proved sm,SM=0,10 "
} }
if 2 <= v && v <= 10 && 0 <= s && s <= 3 { if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
proveu(x) // ERROR "Proved sm,SM=0,10 " proveu(x) // ERROR "Proved sm,SM=0,10 "
} }
if 2 <= v && v <= 10 && 1 <= s && s <= 3 { if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
proveu(x) // ERROR "Proved sm,SM=0,5 " proveu(x) // ERROR "Proved sm,SM=0,5 "
} }
if 20 <= v && v <= 100 && 1 <= s && s <= 3 { if 20 <= v && v <= 100 && 1 <= s && s <= 3 {
x := v>>s // ERROR "Proved" x := v >> s // ERROR "Proved"
proveu(x) // ERROR "Proved sm,SM=2,50 " proveu(x) // ERROR "Proved sm,SM=2,50 "
} }
} }