Base64.java

Base64.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

byte[] decode(String)

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
presumption	java.lang.String:charAt(...)@473 <= 255
presumption	java.lang.String:charAt(...)@482 <= 255
presumption	java.lang.String:charAt(...)@494 <= 255
post	new byte[](decode#1) num objects <= 1
post	new byte[](decode#1).length == 0
post	new byte[](decode#2) num objects <= 1
post	new byte[](decode#2).length in {0, 3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 42, 45, 48, 51, 54, 57, 60, 63, 66, 69, 72, 75, 78, 81, 84, 87, 90, 93, 96, 99, 102, 105, 108, 111, 114, 117, 120, 123, 126, 129, 132, 135, 138, 141, 144, 147, 150...
post	possibly_updated(new byte[](decode#2)[...])
post	return_value in Addr_Set{null,&new byte[](decode#2),&new byte[](decode#1)}
test_vector	IA[...]: {1..2³²-1}, {-2³¹. .-1}
test_vector	java.lang.String:charAt(...)@483: {0..60, 62..2¹⁶-1}, {61}

byte[] decode(byte[])

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
pre	(soft) init'ed(sArr[...])
pre	(soft) sArr.length in {1..2³²-1}
pre	sArr != null
post	new byte[](decode#1) num objects <= 1
post	new byte[](decode#1).length in {0, 3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 42, 45, 48, 51, 54, 57, 60, 63, 66, 69, 72, 75, 78, 81, 84, 87, 90, 93, 96, 99, 102, 105, 108, 111, 114, 117, 120, 123, 126, 129, 132, 135, 138, 141, 144, 147, 150...
post	possibly_updated(new byte[](decode#1)[...])
post	return_value in Addr_Set{null,&new byte[](decode#1)}
test_vector	IA[...]: {1..2³²-1}, {-2³¹.. -1}
test_vector	sArr[...]: {-128..60, 62..255}, {61}

byte[] decode(char[])

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
pre	(soft) sArr.length <= 2³²-1
pre	(soft) sArr[...] <= 255
post	new byte[](decode#1) num objects <= 1
post	new byte[](decode#1).length == 0
post	new byte[](decode#2) num objects <= 1
post	new byte[](decode#2).length in {0, 3, 6, 9, 12, 15, 18, 21, 24, 27, 30, 33, 36, 39, 42, 45, 48, 51, 54, 57, 60, 63, 66, 69, 72, 75, 78, 81, 84, 87, 90, 93, 96, 99, 102, 105, 108, 111, 114, 117, 120, 123, 126, 129, 132, 135, 138, 141, 144, 147, 150...
post	possibly_updated(new byte[](decode#2)[...])
post	return_value in Addr_Set{null,&new byte[](decode#2),&new byte[](decode#1)}
test_vector	IA[...]: {1..2³²-1}, {-2³¹. .-1}
test_vector	sArr[...]: {0..60, 62..255}, {61}

byte[] decodeFast(String)

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
pre	s != null
presumption	java.lang.String:charAt(...)@549 <= 255
presumption	java.lang.String:charAt(...)@567 <= 255
presumption	java.lang.String:length(...)@523 not in {1..3}
post	new byte[](decodeFast#1) num objects <= 1
post	new byte[](decodeFast#1).length == 0
post	new byte[](decodeFast#2) num objects <= 1
post	new byte[](decodeFast#2).length <= 2³¹
post	possibly_updated(new byte[](decodeFast#2)[...])
post	return_value in Addr_Set{&new byte[](decodeFast #2),&new byte[](decodeFast#1)}
test_vector	IA[...]: {0..2³²-1}, {-2³¹. .-1}
test_vector	java.lang.String:length(...)@523: {77.. 2³²-1}, {0}

byte[] decodeFast(byte[])

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
pre	(soft) sArr[...] >= 0
pre	(soft) sArr[76] >= 0
pre	sArr != null
pre	sArr.length in {0, 4..2³²-1}
post	new byte[](decodeFast#1) num objects <= 1
post	new byte[](decodeFast#1).length == 0
post	new byte[](decodeFast#2) num objects <= 1
post	new byte[](decodeFast#2).length <= 2³¹
post	possibly_updated(new byte[](decodeFast#2)[...])
post	return_value in Addr_Set{&new byte[](decodeFast #2),&new byte[](decodeFast#1)}
test_vector	IA[...]: {0..2³²-1}, {-2³¹.. -1}
test_vector	sArr.length: {77..2³²-1}, {0}

byte[] decodeFast(char[])

Kind	Annotation Text
pre	(soft) init'ed(IA[...])
pre	(soft) sArr[...] <= 255
pre	(soft) sArr[76] <= 255
pre	sArr != null
pre	sArr.length in {0, 4..2³²-1}
post	new byte[](decodeFast#1) num objects <= 1
post	new byte[](decodeFast#1).length == 0
post	new byte[](decodeFast#2) num objects <= 1
post	new byte[](decodeFast#2).length <= 2³¹
post	possibly_updated(new byte[](decodeFast#2)[...])
post	return_value in Addr_Set{&new byte[](decodeFast #2),&new byte[](decodeFast#1)}
test_vector	IA[...]: {0..2³²-1}, {-2³¹. .-1}
test_vector	sArr.length: {77..2³²-1}, {0}

byte[] encodeToByte(byte[], bool)

Kind	Annotation Text
pre	(soft) init'ed(sArr[...])
pre	(soft) sArr.length in {0, 3..132_343_121}
presumption	(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024) mod 64 < java.lang.String:toCharArray(...)@75.length
presumption	(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256) mod 64 < java.lang.String:toCharArray(.. .)@75.length
presumption	init'ed(java.lang.String:toCharArray(...)@75[...])
presumption	java.lang.String:toCharArray(...)@75.length >= 1
presumption	shr(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024, 12) < java.lang.String:toCharArray(...)@75.length
presumption	ushr(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024, 6) mod 64 < java.lang.String:toCharArray(...)@75. length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 12) mod 64 < java.lang. String:toCharArray(...)@75.length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 18) mod 64 < java.lang. String:toCharArray(...)@75.length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 6) mod 64 < java.lang. String:toCharArray(...)@75.length
post	new byte[](encodeToByte#1) num objects <= 1
post	new byte[](encodeToByte#1).length == 0
post	new byte[](encodeToByte#2) num objects <= 1
post	new byte[](encodeToByte#2).length == (((One-of{sArr.length, 0} - 1)/3)4 + 4) mod 2³² + One-of{((((((One-of{sArr.length, 0} - 1)/3)4 + 4) mod 2³² - 1)/76)*2) mod 2³², 0}
post	new byte[](encodeToByte#2).length in {4..181_101_114}
post	possibly_updated(new byte[](encodeToByte#2)[...])
post	return_value in Addr_Set{&new byte[](encodeToBy te#2),&new byte[](encodeToByte#1)}
test_vector	lineSep: {0}, {1}

char[] encodeToChar(byte[], bool)

Kind	Annotation Text
pre	(soft) init'ed(sArr[...])
pre	(soft) sArr.length in {0, 3..169_538_366}
presumption	(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024) mod 64 < java.lang.String:toCharArray(...)@75.length
presumption	(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256) mod 64 < java.lang.String:toCharArray(.. .)@75.length
presumption	init'ed(java.lang.String:toCharArray(...)@75[...])
presumption	java.lang.String:toCharArray(...)@75.length >= 1
presumption	shr(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024, 12) < java.lang.String:toCharArray(...)@75.length
presumption	ushr(((sArr[(sLen - 1)] mod 256)4) mod 2³² \| (sArr[eLen] mod 256)1_024, 6) mod 64 < java.lang.String:toCharArray(...)@75. length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 12) mod 64 < java.lang. String:toCharArray(...)@75.length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 18) mod 64 < java.lang. String:toCharArray(...)@75.length
presumption	ushr(sArr[s] \| (sArr[s] mod 256)2¹⁶ \| (sArr[s] mod 256)256, 6) mod 64 < java.lang. String:toCharArray(...)@75.length
post	new char[](encodeToChar#1) num objects <= 1
post	new char[](encodeToChar#1).length == 0
post	new char[](encodeToChar#2) num objects <= 1
post	new char[](encodeToChar#2).length == (((One-of{sArr.length, 0} - 1)/3)4 + 4) mod 2³² + One-of{((((((One-of{sArr.length, 0} - 1)/3)4 + 4) mod 2³² - 1)/76)*2) mod 2³², 0}
post	new char[](encodeToChar#2).length in {4..231_999_870}
post	possibly_updated(new char[](encodeToChar#2)[...])
post	return_value in Addr_Set{&new char[](encodeToCh ar#2),&new char[](encodeToChar#1)}
test_vector	lineSep: {0}, {1}

String encodeToString(byte[], bool)

Kind	Annotation Text
pre	(soft) init'ed(sArr[...])
pre	(soft) sArr.length in {0, 3..169_538_366}
post	new String(encodeToString#1) num objects == 1
post	return_value == &new String(encodeToString#1)

void net.miginfocom.Base64()

Kind	Annotation Text

net.miginfocom.Base64__static_init

Kind	Annotation Text
presumption	CA.length@75 <= 2³²-1
presumption	CA[i]@75 <= 255
post	CA != null
post	IA == &new int[](Base64__static_init#1)
post	IA.length == 256
post	IA[61] == 0
post	init'ed(IA[...])
post	new int[](Base64__static_init#1) num objects == 1