integerHeader -- Documentation

numbers

numbers;defined in: integerHeader.key Line: 6 Offset :4

int

int;defined in: integerHeader.key Line: 7 Offset :4

real

real;defined in: integerHeader.key Line: 13 Offset :4

#

numbers # ; defined in: integerHeader.key Line: 23 Offset :4

0

numbers 0 (numbers ); defined in: integerHeader.key Line: 24 Offset :4

1

numbers 1 (numbers ); defined in: integerHeader.key Line: 25 Offset :4

2

numbers 2 (numbers ); defined in: integerHeader.key Line: 26 Offset :4

3

numbers 3 (numbers ); defined in: integerHeader.key Line: 27 Offset :4

4

numbers 4 (numbers ); defined in: integerHeader.key Line: 28 Offset :4

5

numbers 5 (numbers ); defined in: integerHeader.key Line: 29 Offset :4

6

numbers 6 (numbers ); defined in: integerHeader.key Line: 30 Offset :4

7

numbers 7 (numbers ); defined in: integerHeader.key Line: 31 Offset :4

8

numbers 8 (numbers ); defined in: integerHeader.key Line: 32 Offset :4

9

numbers 9 (numbers ); defined in: integerHeader.key Line: 33 Offset :4

neglit

numbers neglit (numbers ); defined in: integerHeader.key Line: 34 Offset :4

Z

int Z (numbers ); defined in: integerHeader.key Line: 36 Offset :4

C

int C (numbers ); defined in: integerHeader.key Line: 37 Offset :4

add

int add (int , int ); defined in: integerHeader.key Line: 40 Offset :4

neg

int neg (int ); defined in: integerHeader.key Line: 41 Offset :4

sub

int sub (int , int ); defined in: integerHeader.key Line: 42 Offset :4

mul

int mul (int , int ); defined in: integerHeader.key Line: 43 Offset :4

div

int div (int , int ); defined in: integerHeader.key Line: 44 Offset :4

mod

int mod (int , int ); defined in: integerHeader.key Line: 45 Offset :4

pow

int pow (int , int ); defined in: integerHeader.key Line: 46 Offset :4

log

int log (int , int ); defined in: integerHeader.key Line: 47 Offset :4

bsum

int bsum {false , false , true } (int , int , int ); defined in: integerHeader.key Line: 50 Offset :4

bprod

int bprod {false , false , true } (int , int , int ); defined in: integerHeader.key Line: 51 Offset :4

sum

int sum {true , true } (boolean , int ); defined in: integerHeader.key Line: 52 Offset :4

prod

int prod {true , true } (boolean , int ); defined in: integerHeader.key Line: 53 Offset :4

min

int min {true , true } (boolean , int ); defined in: integerHeader.key Line: 54 Offset :4

max

int max {true , true } (boolean , int ); defined in: integerHeader.key Line: 55 Offset :4

byte_MAX

int byte_MAX ; defined in: integerHeader.key Line: 58 Offset :4

byte_MIN

int byte_MIN ; defined in: integerHeader.key Line: 59 Offset :4

char_MAX

int char_MAX ; defined in: integerHeader.key Line: 60 Offset :4

char_MIN

int char_MIN ; defined in: integerHeader.key Line: 61 Offset :4

int_MAX

int int_MAX ; defined in: integerHeader.key Line: 62 Offset :4

int_MIN

int int_MIN ; defined in: integerHeader.key Line: 63 Offset :4

long_MAX

int long_MAX ; defined in: integerHeader.key Line: 64 Offset :4

long_MIN

int long_MIN ; defined in: integerHeader.key Line: 65 Offset :4

short_MAX

int short_MAX ; defined in: integerHeader.key Line: 66 Offset :4

short_MIN

int short_MIN ; defined in: integerHeader.key Line: 67 Offset :4

byte_HALFRANGE

int byte_HALFRANGE ; defined in: integerHeader.key Line: 70 Offset :4

byte_RANGE

int byte_RANGE ; defined in: integerHeader.key Line: 71 Offset :4

char_RANGE

int char_RANGE ; defined in: integerHeader.key Line: 72 Offset :4

int_HALFRANGE

int int_HALFRANGE ; defined in: integerHeader.key Line: 73 Offset :4

int_RANGE

int int_RANGE ; defined in: integerHeader.key Line: 74 Offset :4

long_HALFRANGE

int long_HALFRANGE ; defined in: integerHeader.key Line: 75 Offset :4

long_RANGE

int long_RANGE ; defined in: integerHeader.key Line: 76 Offset :4

short_HALFRANGE

int short_HALFRANGE ; defined in: integerHeader.key Line: 77 Offset :4

short_RANGE

int short_RANGE ; defined in: integerHeader.key Line: 78 Offset :4

undefinedPow

int undefinedPow (int , int ); defined in: integerHeader.key Line: 81 Offset :4

undefinedLog

int undefinedLog (int , int ); defined in: integerHeader.key Line: 82 Offset :4

javaUnaryMinusIntOverFlow

int javaUnaryMinusIntOverFlow (int ); defined in: integerHeader.key Line: 85 Offset :4

javaUnaryMinusLongOverFlow

int javaUnaryMinusLongOverFlow (int ); defined in: integerHeader.key Line: 86 Offset :4

javaAddIntOverFlow

int javaAddIntOverFlow (int , int ); defined in: integerHeader.key Line: 87 Offset :4

javaAddLongOverFlow

int javaAddLongOverFlow (int , int ); defined in: integerHeader.key Line: 88 Offset :4

javaSubIntOverFlow

int javaSubIntOverFlow (int , int ); defined in: integerHeader.key Line: 89 Offset :4

javaSubLongOverFlow

int javaSubLongOverFlow (int , int ); defined in: integerHeader.key Line: 90 Offset :4

javaMulIntOverFlow

int javaMulIntOverFlow (int , int ); defined in: integerHeader.key Line: 91 Offset :4

javaMulLongOverFlow

int javaMulLongOverFlow (int , int ); defined in: integerHeader.key Line: 92 Offset :4

javaModOverFlow

int javaModOverFlow (int , int ); defined in: integerHeader.key Line: 93 Offset :4

javaDivIntOverFlow

int javaDivIntOverFlow (int , int ); defined in: integerHeader.key Line: 94 Offset :4

javaDivLongOverFlow

int javaDivLongOverFlow (int , int ); defined in: integerHeader.key Line: 95 Offset :4

javaUnsignedShiftRightOverFlow

int javaUnsignedShiftRightOverFlow (int , int ); defined in: integerHeader.key Line: 96 Offset :4

javaBitwiseOrIntOverFlow

int javaBitwiseOrIntOverFlow (int , int ); defined in: integerHeader.key Line: 97 Offset :4

javaCastByteOverFlow

int javaCastByteOverFlow (int ); defined in: integerHeader.key Line: 98 Offset :4

javaCastShortOverFlow

int javaCastShortOverFlow (int ); defined in: integerHeader.key Line: 99 Offset :4

javaCastIntOverFlow

int javaCastIntOverFlow (int ); defined in: integerHeader.key Line: 100 Offset :4

javaCastLongOverFlow

int javaCastLongOverFlow (int ); defined in: integerHeader.key Line: 101 Offset :4

javaCastCharOverFlow

int javaCastCharOverFlow (int ); defined in: integerHeader.key Line: 102 Offset :4

jmod

int jmod (int , int ); defined in: integerHeader.key Line: 105 Offset :4

jdiv

int jdiv (int , int ); defined in: integerHeader.key Line: 106 Offset :4

unaryMinusJint

int unaryMinusJint (int ); defined in: integerHeader.key Line: 107 Offset :4

unaryMinusJlong

int unaryMinusJlong (int ); defined in: integerHeader.key Line: 108 Offset :4

addJint

int addJint (int , int ); defined in: integerHeader.key Line: 109 Offset :4

addJlong

int addJlong (int , int ); defined in: integerHeader.key Line: 110 Offset :4

subJint

int subJint (int , int ); defined in: integerHeader.key Line: 111 Offset :4

subJlong

int subJlong (int , int ); defined in: integerHeader.key Line: 112 Offset :4

mulJint

int mulJint (int , int ); defined in: integerHeader.key Line: 113 Offset :4

mulJlong

int mulJlong (int , int ); defined in: integerHeader.key Line: 114 Offset :4

modJint

int modJint (int , int ); defined in: integerHeader.key Line: 115 Offset :4

modJlong

int modJlong (int , int ); defined in: integerHeader.key Line: 116 Offset :4

divJint

int divJint (int , int ); defined in: integerHeader.key Line: 117 Offset :4

divJlong

int divJlong (int , int ); defined in: integerHeader.key Line: 118 Offset :4

moduloByte

int moduloByte (int ); defined in: integerHeader.key Line: 119 Offset :4

moduloShort

int moduloShort (int ); defined in: integerHeader.key Line: 120 Offset :4

moduloInt

int moduloInt (int ); defined in: integerHeader.key Line: 121 Offset :4

moduloLong

int moduloLong (int ); defined in: integerHeader.key Line: 122 Offset :4

moduloChar

int moduloChar (int ); defined in: integerHeader.key Line: 123 Offset :4

bitwiseNegateJint

int bitwiseNegateJint (int ); defined in: integerHeader.key Line: 126 Offset :4

bitwiseNegateJlong

int bitwiseNegateJlong (int ); defined in: integerHeader.key Line: 127 Offset :4

shiftright

int shiftright (int , int ); defined in: integerHeader.key Line: 132 Offset :4

shiftleft

int shiftleft (int , int ); defined in: integerHeader.key Line: 134 Offset :4

shiftrightPositiveShift

int shiftrightPositiveShift (int , int ); defined in: integerHeader.key Line: 137 Offset :4

shiftleftPositiveShift

int shiftleftPositiveShift (int , int ); defined in: integerHeader.key Line: 139 Offset :4

unsignedshift

int unsignedshift (int , int , int ); defined in: integerHeader.key Line: 143 Offset :4

shiftrightJint

int shiftrightJint (int , int ); defined in: integerHeader.key Line: 147 Offset :4

shiftleftJint

int shiftleftJint (int , int ); defined in: integerHeader.key Line: 148 Offset :4

shiftleftJlong

int shiftleftJlong (int , int ); defined in: integerHeader.key Line: 150 Offset :4

shiftrightJlong

int shiftrightJlong (int , int ); defined in: integerHeader.key Line: 151 Offset :4

unsignedshiftrightJint

int unsignedshiftrightJint (int , int ); defined in: integerHeader.key Line: 153 Offset :4

unsignedshiftrightJlong

int unsignedshiftrightJlong (int , int ); defined in: integerHeader.key Line: 154 Offset :4

binaryAnd

int binaryAnd (int , int ); defined in: integerHeader.key Line: 157 Offset :4

binaryOr

int binaryOr (int , int ); defined in: integerHeader.key Line: 158 Offset :4

binaryXOr

int binaryXOr (int , int ); defined in: integerHeader.key Line: 159 Offset :4

orJint

int orJint (int , int ); defined in: integerHeader.key Line: 162 Offset :4

orJlong

int orJlong (int , int ); defined in: integerHeader.key Line: 163 Offset :4

andJint

int andJint (int , int ); defined in: integerHeader.key Line: 164 Offset :4

andJlong

int andJlong (int , int ); defined in: integerHeader.key Line: 165 Offset :4

xorJint

int xorJint (int , int ); defined in: integerHeader.key Line: 166 Offset :4

xorJlong

int xorJlong (int , int ); defined in: integerHeader.key Line: 167 Offset :4

index

int index ; defined in: integerHeader.key Line: 170 Offset :4

javaUnaryMinusInt

int javaUnaryMinusInt (int ); defined in: integerHeader.key Line: 177 Offset :4

javaUnaryMinusLong

int javaUnaryMinusLong (int ); defined in: integerHeader.key Line: 178 Offset :4

javaBitwiseNegateInt

int javaBitwiseNegateInt (int ); defined in: integerHeader.key Line: 179 Offset :4

javaBitwiseNegateLong

int javaBitwiseNegateLong (int ); defined in: integerHeader.key Line: 180 Offset :4

javaAddInt

int javaAddInt (int , int ); defined in: integerHeader.key Line: 181 Offset :4

javaAddLong

int javaAddLong (int , int ); defined in: integerHeader.key Line: 182 Offset :4

javaSubInt

int javaSubInt (int , int ); defined in: integerHeader.key Line: 183 Offset :4

javaSubLong

int javaSubLong (int , int ); defined in: integerHeader.key Line: 184 Offset :4

javaMulInt

int javaMulInt (int , int ); defined in: integerHeader.key Line: 185 Offset :4

javaMulLong

int javaMulLong (int , int ); defined in: integerHeader.key Line: 186 Offset :4

javaMod

int javaMod (int , int ); defined in: integerHeader.key Line: 187 Offset :4

javaDivInt

int javaDivInt (int , int ); defined in: integerHeader.key Line: 188 Offset :4

javaDivLong

int javaDivLong (int , int ); defined in: integerHeader.key Line: 189 Offset :4

javaShiftRightInt

int javaShiftRightInt (int , int ); defined in: integerHeader.key Line: 190 Offset :4

javaShiftRightLong

int javaShiftRightLong (int , int ); defined in: integerHeader.key Line: 191 Offset :4

javaShiftLeftInt

int javaShiftLeftInt (int , int ); defined in: integerHeader.key Line: 192 Offset :4

javaShiftLeftLong

int javaShiftLeftLong (int , int ); defined in: integerHeader.key Line: 193 Offset :4

javaUnsignedShiftRightInt

int javaUnsignedShiftRightInt (int , int ); defined in: integerHeader.key Line: 194 Offset :4

javaUnsignedShiftRightLong

int javaUnsignedShiftRightLong (int , int ); defined in: integerHeader.key Line: 195 Offset :4

javaBitwiseOrInt

int javaBitwiseOrInt (int , int ); defined in: integerHeader.key Line: 196 Offset :4

javaBitwiseOrLong

int javaBitwiseOrLong (int , int ); defined in: integerHeader.key Line: 197 Offset :4

javaBitwiseAndInt

int javaBitwiseAndInt (int , int ); defined in: integerHeader.key Line: 198 Offset :4

javaBitwiseAndLong

int javaBitwiseAndLong (int , int ); defined in: integerHeader.key Line: 199 Offset :4

javaBitwiseXOrInt

int javaBitwiseXOrInt (int , int ); defined in: integerHeader.key Line: 200 Offset :4

javaBitwiseXOrLong

int javaBitwiseXOrLong (int , int ); defined in: integerHeader.key Line: 201 Offset :4

javaCastByte

int javaCastByte (int ); defined in: integerHeader.key Line: 202 Offset :4

javaCastShort

int javaCastShort (int ); defined in: integerHeader.key Line: 203 Offset :4

javaCastInt

int javaCastInt (int ); defined in: integerHeader.key Line: 204 Offset :4

javaCastLong

int javaCastLong (int ); defined in: integerHeader.key Line: 205 Offset :4

javaCastChar

int javaCastChar (int ); defined in: integerHeader.key Line: 206 Offset :4

checkedUnaryMinusInt

int checkedUnaryMinusInt (int ); defined in: integerHeader.key Line: 212 Offset :4

checkedUnaryMinusLong

int checkedUnaryMinusLong (int ); defined in: integerHeader.key Line: 213 Offset :4

checkedBitwiseNegateInt

int checkedBitwiseNegateInt (int ); defined in: integerHeader.key Line: 214 Offset :4

checkedBitwiseNegateLong

int checkedBitwiseNegateLong (int ); defined in: integerHeader.key Line: 215 Offset :4

checkedAddInt

int checkedAddInt (int , int ); defined in: integerHeader.key Line: 216 Offset :4

checkedAddLong

int checkedAddLong (int , int ); defined in: integerHeader.key Line: 217 Offset :4

checkedSubInt

int checkedSubInt (int , int ); defined in: integerHeader.key Line: 218 Offset :4

checkedSubLong

int checkedSubLong (int , int ); defined in: integerHeader.key Line: 219 Offset :4

checkedMulInt

int checkedMulInt (int , int ); defined in: integerHeader.key Line: 220 Offset :4

checkedMulLong

int checkedMulLong (int , int ); defined in: integerHeader.key Line: 221 Offset :4

checkedDivInt

int checkedDivInt (int , int ); defined in: integerHeader.key Line: 222 Offset :4

checkedDivLong

int checkedDivLong (int , int ); defined in: integerHeader.key Line: 223 Offset :4

checkedShiftRightInt

int checkedShiftRightInt (int , int ); defined in: integerHeader.key Line: 224 Offset :4

checkedShiftRightLong

int checkedShiftRightLong (int , int ); defined in: integerHeader.key Line: 225 Offset :4

checkedShiftLeftInt

int checkedShiftLeftInt (int , int ); defined in: integerHeader.key Line: 226 Offset :4

checkedShiftLeftLong

int checkedShiftLeftLong (int , int ); defined in: integerHeader.key Line: 227 Offset :4

checkedUnsignedShiftRightInt

int checkedUnsignedShiftRightInt (int , int ); defined in: integerHeader.key Line: 228 Offset :4

checkedUnsignedShiftRightLong

int checkedUnsignedShiftRightLong (int , int ); defined in: integerHeader.key Line: 229 Offset :4

checkedBitwiseOrInt

int checkedBitwiseOrInt (int , int ); defined in: integerHeader.key Line: 230 Offset :4

checkedBitwiseOrLong

int checkedBitwiseOrLong (int , int ); defined in: integerHeader.key Line: 231 Offset :4

checkedBitwiseAndInt

int checkedBitwiseAndInt (int , int ); defined in: integerHeader.key Line: 232 Offset :4

checkedBitwiseAndLong

int checkedBitwiseAndLong (int , int ); defined in: integerHeader.key Line: 233 Offset :4

checkedBitwiseXOrInt

int checkedBitwiseXOrInt (int , int ); defined in: integerHeader.key Line: 234 Offset :4

checkedBitwiseXOrLong

int checkedBitwiseXOrLong (int , int ); defined in: integerHeader.key Line: 235 Offset :4

leq

leq (int , int ); defined in: integerHeader.key Line: 245 Offset :4

lt

lt (int , int ); defined in: integerHeader.key Line: 246 Offset :4

geq

geq (int , int ); defined in: integerHeader.key Line: 247 Offset :4

gt

gt (int , int ); defined in: integerHeader.key Line: 248 Offset :4

inByte

inByte (int ); defined in: integerHeader.key Line: 255 Offset :4

inChar

inChar (int ); defined in: integerHeader.key Line: 256 Offset :4

inInt

inInt (int ); defined in: integerHeader.key Line: 257 Offset :4

inLong

inLong (int ); defined in: integerHeader.key Line: 258 Offset :4

inShort

inShort (int ); defined in: integerHeader.key Line: 259 Offset :4

inRangeByte

inRangeByte (int ); defined in: integerHeader.key Line: 266 Offset :4

inRangeChar

inRangeChar (int ); defined in: integerHeader.key Line: 267 Offset :4

inRangeInt

inRangeInt (int ); defined in: integerHeader.key Line: 268 Offset :4

inRangeLong

inRangeLong (int ); defined in: integerHeader.key Line: 269 Offset :4

inRangeShort

inRangeShort (int ); defined in: integerHeader.key Line: 270 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview

integerHeader.key

Sorts