From 938abfc6f733080a52593577624fef30c1ddf301 Mon Sep 17 00:00:00 2001
From: Koen Wermer <koenwermer@gmail.com>
Date: Fri, 10 Feb 2017 13:01:52 +0100
Subject: [PATCH] added support for bit vector operations and pre processed the
test files
---
HelperFunctions.hs | 5 +-
...eturnValueVar == returnValue_False_False_1 | 16 +
...returnValueVar == returnValue_True_False_1 | 15 +
...eturnValueVar == returnValue_False_False_1 | 16 +
...dientfunction_true_true_true_False_False_1 | 14 +
...eturnValueVar == returnValue_False_False_1 | 30 ++
Results/iterator_true_true_true_False_False_1 | 23 ++
Settings.hs | 20 +-
Tests/GradientFunction.class | Bin 0 -> 2475 bytes
Tests/GradientFunction.java | 14 +-
Tests/Iterator.class | Bin 0 -> 2704 bytes
Tests/Iterator.java | 119 ++++++
Tests/OpenIntToDoubleHashMap.java | 376 +++++++++---------
Tests/arrays1.class | Bin 9377 -> 2569 bytes
Tests/arrays1.java | 2 +-
Verifier.hs | 43 +-
16 files changed, 479 insertions(+), 214 deletions(-)
create mode 100644 Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_False_False_1
create mode 100644 Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_True_False_1
create mode 100644 Results/gradientfunction_true_returnValueVar == returnValue_returnValueVar == returnValue_False_False_1
create mode 100644 Results/gradientfunction_true_true_true_False_False_1
create mode 100644 Results/iterator_true_returnValue != null_returnValueVar == returnValue_False_False_1
create mode 100644 Results/iterator_true_true_true_False_False_1
create mode 100644 Tests/GradientFunction.class
create mode 100644 Tests/Iterator.class
create mode 100644 Tests/Iterator.java
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index b380bfe..3580e2a 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -23,6 +23,7 @@ lookupType decls env (Name idents) = case lookup (Name [head idents]) env of
-- | Gets the type of a field of an object of given type
getFieldType :: [TypeDecl] -> Type -> Name -> Type
getFieldType _ t (Name []) = t
+getFieldType _ _ (Name [Ident "length"]) = PrimType IntT
getFieldType decls (RefType (ClassRefType t)) (Name (f:fs)) = getFieldType decls (getFieldTypeFromClassDecl (getDecl t decls) f) (Name fs)
where
getFieldTypeFromClassDecl :: ClassDecl -> Ident -> Type
@@ -192,10 +193,10 @@ false = Lit (Boolean False)
-- Logical operators for expressions:
(&*) :: Exp -> Exp -> Exp
-e1 &* e2 = BinOp e1 And e2
+e1 &* e2 = BinOp e1 CAnd e2
(|*) :: Exp -> Exp -> Exp
-e1 |* e2 = BinOp e1 Or e2
+e1 |* e2 = BinOp e1 COr e2
neg :: Exp -> Exp
neg = PreNot
diff --git a/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_False_False_1
new file mode 100644
index 0000000..d0c7864
--- /dev/null
+++ b/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_False_False_1
@@ -0,0 +1,16 @@
+testFile: gradientfunction
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+6 value
+5 value
+4 value
+2 value
+11 value
+10 value
+Total number of mutants: 26
+Number of mutants in which we found an error: 6
\ No newline at end of file
diff --git a/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_True_False_1 b/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_True_False_1
new file mode 100644
index 0000000..a4cce7e
--- /dev/null
+++ b/Results/gradientfunction_true_returnValue != null_returnValueVar == returnValue_True_False_1
@@ -0,0 +1,15 @@
+testFile: gradientfunction
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: True
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+6 value
+5 value
+4 value
+2 value
+11 value
+Total number of mutants: 26
+Number of mutants in which we found an error: 5
\ No newline at end of file
diff --git a/Results/gradientfunction_true_returnValueVar == returnValue_returnValueVar == returnValue_False_False_1 b/Results/gradientfunction_true_returnValueVar == returnValue_returnValueVar == returnValue_False_False_1
new file mode 100644
index 0000000..5f12fa9
--- /dev/null
+++ b/Results/gradientfunction_true_returnValueVar == returnValue_returnValueVar == returnValue_False_False_1
@@ -0,0 +1,16 @@
+testFile: gradientfunction
+postCondVoid: true
+postCondRefType: returnValueVar == returnValue
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+6 value
+5 value
+4 value
+2 value
+11 value
+10 value
+Total number of mutants: 26
+Number of mutants in which we found an error: 6
\ No newline at end of file
diff --git a/Results/gradientfunction_true_true_true_False_False_1 b/Results/gradientfunction_true_true_true_False_False_1
new file mode 100644
index 0000000..b4b5559
--- /dev/null
+++ b/Results/gradientfunction_true_true_true_False_False_1
@@ -0,0 +1,14 @@
+testFile: gradientfunction
+postCondVoid: true
+postCondRefType: true
+postCondPrimType: true
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+6 value
+5 value
+4 value
+2 value
+Total number of mutants: 26
+Number of mutants in which we found an error: 4
\ No newline at end of file
diff --git a/Results/iterator_true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/iterator_true_returnValue != null_returnValueVar == returnValue_False_False_1
new file mode 100644
index 0000000..179bdce
--- /dev/null
+++ b/Results/iterator_true_returnValue != null_returnValueVar == returnValue_False_False_1
@@ -0,0 +1,30 @@
+testFile: iterator
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+9 hasNext
+8 hasNext
+7 hasNext
+6 hasNext
+42 advance
+41 advance
+39 advance
+32 advance
+31 advance
+28 value
+26 value
+25 value
+23 value
+22 value
+19 key
+17 key
+16 key
+14 key
+13 key
+10 hasNext
+Total number of mutants: 43
+Number of mutants in which we found an error: 20
\ No newline at end of file
diff --git a/Results/iterator_true_true_true_False_False_1 b/Results/iterator_true_true_true_False_False_1
new file mode 100644
index 0000000..57ea176
--- /dev/null
+++ b/Results/iterator_true_true_true_False_False_1
@@ -0,0 +1,23 @@
+testFile: iterator
+postCondVoid: true
+postCondRefType: true
+postCondPrimType: true
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+erronous mutations detected:
+42 advance
+41 advance
+39 advance
+32 advance
+31 advance
+26 value
+25 value
+23 value
+22 value
+17 key
+16 key
+14 key
+13 key
+Total number of mutants: 43
+Number of mutants in which we found an error: 13
\ No newline at end of file
diff --git a/Settings.hs b/Settings.hs
index b241d71..d246977 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -3,12 +3,12 @@ module Settings where
import System.FilePath(joinPath)
testFile, postCondVoid, postCondRefType, postCondPrimType :: String
-testFile = "basesecantsolver"
+testFile = test3
-- The post condition may depend on the type of the method we are looking at
postCondVoid = "true"
-postCondRefType = "returnValue != null"
-postCondPrimType = "returnValueVar == returnValue"
+postCondRefType = heur1
+postCondPrimType = heur2
-- When ignoreLibMethods is true, library calls will simply be ignored. When false, we consider library methods but make no assumptions about them (so the WLP will be true)
-- To prevent insanely long calculation times, we may decide to not calculate the wlp of the main method when ignoring library methods
@@ -23,4 +23,16 @@ nrOfUnroll = 1
-- The classpath for test files
classPath :: FilePath -> FilePath
classPath "basesecantsolver" = joinPath ["org", "apache", "commons", "math3", "analysis", "solvers"]
-classPath _ = ""
\ No newline at end of file
+classPath "gradientfunction" = joinPath ["org", "apache", "commons", "math3", "analysis", "differentiation"]
+classPath "iterator" = joinPath ["org", "apache", "commons", "math3", "util"]
+classPath _ = ""
+
+
+-- Some constants, for convenience:
+test1 = "basesecantsolver"
+test2 = "gradientfunction"
+test3 = "iterator"
+
+heur0 = "true"
+heur1 = "returnValue != null"
+heur2 = "returnValueVar == returnValue"
\ No newline at end of file
diff --git a/Tests/GradientFunction.class b/Tests/GradientFunction.class
new file mode 100644
index 0000000000000000000000000000000000000000..2f0890ce7ada774b1c0eae5a4512209670922587
GIT binary patch
literal 2475
zcmc&!&u<$=6#mBE-LcnpJa*zZcI!fD+S+jvlZ2#gC{ZC!!Kg{9rbH@{h&Il~b?}dB
zV@Kk|rFX;$h=g1Pp}kTBl%EmYQ2z-o95`^|&;yDZ-t0O*Dk@cpijci;-@N(Wd*6IJ
zGY=kpzYSm%7j)=I`Ed%*>13Yw!;fB$7j&pN9Y7z>NbfAiIgT_(hJmdzEL^QyrJQlw
zDBd!2#d@_`udU~*M&s6K&Zrrc_twknxs~$js%e?EM%ieT>$TiWv(hMU7#0o9{K4FE
z#k|t26(!_l2JKS0R&Go(+)V#BEiwxX%2a*DWC&j^*UZ^wb=kCT7(|01G~Y0a@6H&v
zow2j#eg<{Js5EI-OE2a#i+PSL#{fyhG033L*PB++yi%6=v65x1lxfMU?G+8J85>3r
z9T?)s1@R(=gBZbR5J7|(rjIUS-n2+V($So6Sj}RiX_>P8OC0?{#4r}bIL<S?cJ#`x
zx2f-a3<e>|=PE|6l$%>#Gm8y|OHZ$R_%kn1Qr$YJc;o5mN8dFJZ!8{TuRK9X+JBzK
zyfg&{Z(44ZSk+joTe)hp;cnuodTq5_qP?)RG_y22N2h_Hd}?lC`ua3ws_8-@^EO53
zUC7G<AEuubxy&<LWLL>-Tr(^>n3V$+B>BZcCXZga0dz0~=!wdWO810^{0@Z43L0&|
zOA+8)|9!CjFX7olSW&)(_Y-htBTNzHuH!1%uc6#?3Pi|uP$K9~QE&!l=@+F@2Hsu7
z;o<1y=mMknoAm6;q;_oYO`ikZE(hf|V#x{etJ_{x_uF?;M0MNyvfDpFopB)=cOhOI
zNs4fScwDj?xrz<NJ4tat6Pk@rrArgRRCfC_d|+dk0zP-#!uvLQX}pP;Pq<|zZVM$F
ze#d!7rt2+Sb5J3n3!S=e;_^W12dFo*+fF<pe8TUtqW&jkj^Cvvq)+WQu~n2*HZ^=7
z+WZ|avv+0bO+-XM1oqdQknjM(N&Zm(S5OANqt#)y4GoImK2*vhf-aP2w}0dlN*fgt
zp~q371C&0Ywox4-?4pR7!#GSR64GJZLB6BpxF*{~rIbu&ipX7rVw%+Qp^b4F5$#9|
zzuV|@s>g*8QK!0t-NFMKy3E?b&oU*}!n6YniI|8Ha1&z*H70vWMLI>7OKnfgu0zy1
z$#=w@la;z#IMuGyExMgb9SJ3-4JOoY;JYp%iGyYdk@#1$xae`4?di~Ss9AhZhq*f%
zvmZTd6HJPvn?s)|B6}nWN4}a+zL5JJ@{ml@IRgf88iSaj!}1Y^@F)3yVT7eH#-=dN
z%5=$pj6U`UE_g<8(eoB2JT08}e2!P-p<=(_VpPv_#CH%StLvB94uy3Qj;rxqoPgpS
ztsa`Ab1$tA_vp`d>DV7{4v*z&hiWqZH`LBRfg`blF0z3sj-DOF$VxZqxXD03l4MMe
wL=qa2jDzo!q$C0plrCp!CC%f{;>o#QS(%Yq|6_AUsaI*Obj_V`w#3PQ00cfO&Hw-a
literal 0
HcmV?d00001
diff --git a/Tests/GradientFunction.java b/Tests/GradientFunction.java
index 25aa7c7..c85f6cf 100644
--- a/Tests/GradientFunction.java
+++ b/Tests/GradientFunction.java
@@ -33,8 +33,8 @@ public class GradientFunction implements MultivariateVectorFunction {
/** Simple constructor.
* @param f underlying real-valued function
*/
- public GradientFunction(final MultivariateDifferentiableFunction f) {
- this.f = f;
+ public GradientFunction(final MultivariateDifferentiableFunction f1) {
+ this.f = f1;
}
/** {@inheritDoc} */
@@ -47,15 +47,15 @@ public class GradientFunction implements MultivariateVectorFunction {
}
// compute the derivatives
- final DerivativeStructure dsY = f.value(dsX);
+ final DerivativeStructure dsY = this.f.value(dsX);
// extract the gradient
final double[] y = new double[point.length];
final int[] orders = new int[point.length];
- for (int i = 0; i < point.length; ++i) {
- orders[i] = 1;
- y[i] = dsY.getPartialDerivative(orders);
- orders[i] = 0;
+ for (int j = 0; j < point.length; ++j) {
+ orders[j] = 1;
+ y[j] = dsY.getPartialDerivative(orders);
+ orders[j] = 0;
}
return y;
diff --git a/Tests/Iterator.class b/Tests/Iterator.class
new file mode 100644
index 0000000000000000000000000000000000000000..a209b6b574657a7ac5db7235255a081371c700f4
GIT binary patch
literal 2704
zcmb7FNpD+K7(Lh1b37#1&fpBr)TC+RmbxXhWe6orn$XY;>P%at^u>8e+$45z?5JI^
zL!w1u#i}XbP$9hy5(3c{fdqRtY>@Z?h!wC$2-Tc>pBp<gAS%mu_@?`P=X~$p?;m~r
zEr3Bx1Q5k@H8_H!0S?D%5W(|mctH&>1~|NAV93DB0n{kN2#yEfcUG^c?XVh77#J}y
zYT%@RXZ*tCq<|O^2#;nn>v=Pizi6%$EH_US)Gu2%*9BZxCj@*ON}+f3^wBo&?C9)G
zWeb@+1JSNFXDwJcE0eND9ifpb<hZBWld*1a@(rak>HKj4cmKdeN=LKvmO$NPI%7>2
zR_CnTd2?=slJL2_nOdGQ*YsZJJS1Q&nd{R!4&ARX2y@h-cy?gyM#@^tr&$V<(g|x7
z6E@8G4U<W+dfJ`K7IG<TJgtvO=dGNX&*lzZH#f`>_MpeWSP0|j2;o(n3ZY%CI@Qpv
zhC}EP=u*bXLO#8coX(yrq?X23tW{RIoq@nW#f0FNQJBikrx(&GQzf}=8$y=~97A&m
zEocp)4RL{f?Z0AX7LzA(IrHX3X5P9nQ^?OOj1bxR^=)^7zHDwWX|9>6B`cZAuC5Y*
z<f@rp8gw$8C|4*TD=}y0u3IV6(YR_}&*qY=1v1K{lFW4>y-1p7XQyVTX9(Ts%*C;@
zV+7ILKQS?Ig(yVWiePWWQI7^N26rwr@y{Ccnq}yjmFSrma*iq(^_~UmnTT@s(v!F|
zQZE}X2sih@?ZiWf#20XFqR!*_3hp~F+%}?=c((M?NPG#;eRwG`ia4%KgN8xVO<F
zdVP+k%SI~=eDw6#sN>S>1o61;!^f?^h(;%Z->)MWi3c!jcqTt*V#|0N@33SS_A<2&
z7#zFdVZsC0N9_Rh2WXMNEgVE2wI>lS5f5QduZGw7FR?T&aB(AIXUk$o#nQQFDO9-{
z+#?41DPrV=0}Osp-i-V{)06?HklSiqvxO+3@O`9f+aO3eCH9xan_4_e@l{=5T>51|
zqoTd;YV|PHLn??iiAbMRI69EWRWySK5=5!iWfVQ`kF~GI{VCIOpz-Mxk7x)w5DrD%
zQFp8Rk~qy@iB?XHLimPxVPHQ&b7|JoPH`fp;)l23v+=rGhPDu4T3$u<Cz!G^qNKqp
z={+2?ae&fIw8@|h>$JChifFM>`#3@o!EaD=`5^+|sW4G}&Rc33*+Q6B!4HwKkx~*_
zmfXP`HqPkyF)3wK$Je$WV8q5T<)yU|Su5*yf>u`rTCKyF$9+#F;b#&dmBc0@vR>A2
z`!%bx>uF0uLX53XI#>a?iJuEFjB7Z7C5+-1cG~Z}u2j$UqCVKz*d8zfkx0vvn7fSn
z;3<J;Xz3&DHSA}>ZcXk+K~sf-#wxHY6f{&xcTmtEo1TJ#wh9HUPf*aZ8wD-0?LR1p
z$>wb+b>B8uQ4srg3gR;E_|@9b6vS!EwW2_^Pw?<(gw5%3hk`St;4CRPPYN!Of=mCK
z0{1^C;FID|;Ch!=3hzGgn`(m23I!ciU{@$;uafSdpj~!81qEG2wCP3+%P!eP$4vwi
zEZKKoH@56id6fQ8Dec)poSM4CWvV^buJGy{OkCoJnYK$mDTD6a4esHTU3#Do>66{E
zM`yQNq#`=)(tEocQB*nPZTvW?j_E66Tt^GbKG~;JKI&ZfQQ0f^>hON~$VR)e-b*UI
zHX>@>%Qe3&uYBZO`*MG!0TWL&;J|JTI3V}y19ray_Q`&&Rj23%?B|J(FV1~jd-$eQ
z-vR1*xg}zv6|&r42?W?{bL_7a`)iR;%Cd-Iofa9<hOAh?n)n%SieFLCJ$D`*&SxJp
x0$pAG&3rlz|Al6b7x<W*F8@nBM?EeSmmis(x5Tzi2-lx{;C5aU&+6_U{2K*n4`BcR
literal 0
HcmV?d00001
diff --git a/Tests/Iterator.java b/Tests/Iterator.java
new file mode 100644
index 0000000..eda7b85
--- /dev/null
+++ b/Tests/Iterator.java
@@ -0,0 +1,119 @@
+
+// Copied from OpenIntToDoubleHashMap.java
+
+package org.apache.commons.math3.util;
+
+import java.io.IOException;
+import java.io.ObjectInputStream;
+import java.io.Serializable;
+import java.util.ConcurrentModificationException;
+import java.util.NoSuchElementException;
+
+/** Iterator class for the map. */
+public class Iterator {
+
+ protected static final byte FULL = 1;
+ private int[] keys;
+ private double[] values;
+ private byte[] states;
+ private int count;
+
+ /** Reference modification this.count. */
+ private final int referenceCount;
+
+ /** Index of current element. */
+ private int current;
+
+ /** Index of next element. */
+ private int next;
+
+ /**
+ * Simple constructor.
+ */
+ private Iterator() {
+
+ // preserve the modification this.count of the map to detect concurrent modifications later
+ this.referenceCount = this.count;
+
+ // initialize this.current index
+ this.next = -1;
+ try {
+ this.advance();
+ } catch (NoSuchElementException nsee) { // NOPMD
+ // ignored
+ }
+
+ }
+
+ /**
+ * Check if there is a this.next element in the map.
+ * @return true if there is a this.next element
+ */
+ public boolean hasNext() {
+ return this.next >= 0;
+ }
+
+ /**
+ * Get the key of this.current entry.
+ * @return key of this.current entry
+ * @exception ConcurrentModificationException if the map is modified during iteration
+ * @exception NoSuchElementException if there is no element left in the map
+ */
+ public int key()
+ throws ConcurrentModificationException, NoSuchElementException {
+ if (this.referenceCount != this.count) {
+ throw new ConcurrentModificationException();
+ }
+ if (this.current < 0) {
+ throw new NoSuchElementException();
+ }
+ return this.keys[this.current];
+ }
+
+ /**
+ * Get the value of this.current entry.
+ * @return value of this.current entry
+ * @exception ConcurrentModificationException if the map is modified during iteration
+ * @exception NoSuchElementException if there is no element left in the map
+ */
+ public double value()
+ throws ConcurrentModificationException, NoSuchElementException {
+ if (this.referenceCount != this.count) {
+ throw new ConcurrentModificationException();
+ }
+ if (this.current < 0) {
+ throw new NoSuchElementException();
+ }
+ return this.values[this.current];
+ }
+
+ /**
+ * Advance iterator one step further.
+ * @exception ConcurrentModificationException if the map is modified during iteration
+ * @exception NoSuchElementException if there is no element left in the map
+ */
+ public void advance()
+ throws ConcurrentModificationException, NoSuchElementException {
+
+ if (this.referenceCount != this.count) {
+ throw new ConcurrentModificationException();
+ }
+
+ // advance on step
+ this.current = this.next;
+
+ // prepare this.next step
+ try {
+ while (this.states[++this.next] != this.FULL) { // NOPMD
+ // nothing to do
+ }
+ } catch (ArrayIndexOutOfBoundsException e) {
+ this.next = -2;
+ if (this.current < 0) {
+ throw new NoSuchElementException();
+ }
+ }
+
+ }
+
+}
\ No newline at end of file
diff --git a/Tests/OpenIntToDoubleHashMap.java b/Tests/OpenIntToDoubleHashMap.java
index 9fb3e0a..03fa648 100644
--- a/Tests/OpenIntToDoubleHashMap.java
+++ b/Tests/OpenIntToDoubleHashMap.java
@@ -78,29 +78,29 @@ public class OpenIntToDoubleHashMap implements Serializable {
/** Current size of the map. */
private int size;
- /** Bit mask for hash values. */
+ /** Bit mask for hash this.values. */
private int mask;
/** Modifications count. */
private transient int count;
/**
- * Build an empty map with default size and using NaN for missing entries.
+ * Build an empty map with default this.size and using NaN for missing entries.
*/
public OpenIntToDoubleHashMap() {
- this(DEFAULT_EXPECTED_SIZE, Double.NaN);
+ this(this.DEFAULT_EXPECTED_SIZE, Double.NaN);
}
/**
- * Build an empty map with default size
- * @param missingEntries value to return when a missing entry is fetched
+ * Build an empty map with default this.size
+ * @param this.missingEntries value to return when a missing entry is fetched
*/
- public OpenIntToDoubleHashMap(final double missingEntries) {
- this(DEFAULT_EXPECTED_SIZE, missingEntries);
+ public OpenIntToDoubleHashMap(final double missingEntries1) {
+ this(this.DEFAULT_EXPECTED_SIZE, missingEntries1);
}
/**
- * Build an empty map with specified size and using NaN for missing entries.
+ * Build an empty map with specified this.size and using NaN for missing entries.
* @param expectedSize expected number of elements in the map
*/
public OpenIntToDoubleHashMap(final int expectedSize) {
@@ -108,18 +108,18 @@ public class OpenIntToDoubleHashMap implements Serializable {
}
/**
- * Build an empty map with specified size.
+ * Build an empty map with specified this.size.
* @param expectedSize expected number of elements in the map
- * @param missingEntries value to return when a missing entry is fetched
+ * @param this.missingEntries value to return when a missing entry is fetched
*/
- public OpenIntToDoubleHashMap(final int expectedSize,
- final double missingEntries) {
- final int capacity = computeCapacity(expectedSize);
- keys = new int[capacity];
- values = new double[capacity];
- states = new byte[capacity];
- this.missingEntries = missingEntries;
- mask = capacity - 1;
+ public OpenIntToDoubleHashMap(final int expectedSize1,
+ final double missingEntries2) {
+ final int capacity = computeCapacity(expectedSize1);
+ this.keys = new int[capacity];
+ this.values = new double[capacity];
+ this.states = new byte[capacity];
+ this.missingEntries = missingEntries2;
+ this.mask = capacity - 1;
}
/**
@@ -128,33 +128,33 @@ public class OpenIntToDoubleHashMap implements Serializable {
*/
public OpenIntToDoubleHashMap(final OpenIntToDoubleHashMap source) {
final int length = source.keys.length;
- keys = new int[length];
- System.arraycopy(source.keys, 0, keys, 0, length);
- values = new double[length];
- System.arraycopy(source.values, 0, values, 0, length);
- states = new byte[length];
- System.arraycopy(source.states, 0, states, 0, length);
- missingEntries = source.missingEntries;
- size = source.size;
- mask = source.mask;
- count = source.count;
+ this.keys = new int[length];
+ System.arraycopy(source.keys, 0, this.keys, 0, length);
+ this.values = new double[length];
+ System.arraycopy(source.values, 0, this.values, 0, length);
+ this.states = new byte[length];
+ System.arraycopy(source.states, 0, this.states, 0, length);
+ this.missingEntries = source.missingEntries;
+ this.size = source.size;
+ this.mask = source.mask;
+ this.count = source.count;
}
/**
- * Compute the capacity needed for a given size.
- * @param expectedSize expected size of the map
- * @return capacity to use for the specified size
+ * Compute the capacity needed for a given this.size.
+ * @param expectedSize expected this.size of the map
+ * @return capacity to use for the specified this.size
*/
- private static int computeCapacity(final int expectedSize) {
- if (expectedSize == 0) {
+ private static int computeCapacity(final int expectedSize2) {
+ if (expectedSize2 == 0) {
return 1;
}
- final int capacity = (int) FastMath.ceil(expectedSize / LOAD_FACTOR);
- final int powerOfTwo = Integer.highestOneBit(capacity);
- if (powerOfTwo == capacity) {
- return capacity;
+ final int capacity1 = (int) FastMath.ceil(expectedSize2 / this.LOAD_FACTOR);
+ final int powerOfTwo = Integer.highestOneBit(capacity1);
+ if (powerOfTwo == capacity1) {
+ return capacity1;
}
- return nextPowerOfTwo(capacity);
+ return nextPowerOfTwo(capacity1);
}
/**
@@ -171,53 +171,56 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param key key associated with the data
* @return data associated with the key
*/
+ /*
public double get(final int key) {
final int hash = hashOf(key);
- int index = hash & mask;
- if (containsKey(key, index)) {
- return values[index];
+ int index = hash & this.mask;
+ if (this.containsKey1(key, index)) {
+ return this.values[index];
}
- if (states[index] == FREE) {
- return missingEntries;
+ if (this.states[index] == this.FREE) {
+ return this.missingEntries;
}
int j = index;
- for (int perturb = perturb(hash); states[index] != FREE; perturb >>= PERTURB_SHIFT) {
- j = probe(perturb, j);
- index = j & mask;
- if (containsKey(key, index)) {
- return values[index];
+ for (int perturb = perturb(hash); this.states[index] != this.FREE; perturb >>= this.PERTURB_SHIFT) {
+ j = this.probe(perturb, j);
+ index = j & this.mask;
+ if (this.containsKey1(key, index)) {
+ return this.values[index];
}
}
- return missingEntries;
+ return this.missingEntries;
}
+ */
/**
* Check if a value is associated with a key.
* @param key key to check
* @return true if a value is associated with key
*/
- public boolean containsKey(final int key) {
+ /*
+ public boolean containsKey(final int key1) {
- final int hash = hashOf(key);
- int index = hash & mask;
- if (containsKey(key, index)) {
+ final int hash1 = hashOf(key1);
+ int index1 = hash1 & this.mask;
+ if (this.containsKey1(key1, index1)) {
return true;
}
- if (states[index] == FREE) {
+ if (this.states[index1] == this.FREE) {
return false;
}
- int j = index;
- for (int perturb = perturb(hash); states[index] != FREE; perturb >>= PERTURB_SHIFT) {
- j = probe(perturb, j);
- index = j & mask;
- if (containsKey(key, index)) {
+ int j = index1;
+ for (int perturb1 = perturb1(hash1); this.states[index1] != this.FREE; perturb1 >>= this.PERTURB_SHIFT) {
+ j = probe(perturb1, j);
+ index1 = j & this.mask;
+ if (this.containsKey1(key1, index1)) {
return true;
}
}
@@ -225,6 +228,7 @@ public class OpenIntToDoubleHashMap implements Serializable {
return false;
}
+ */
/**
* Get an iterator over map elements.
@@ -242,8 +246,8 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param hash initial hash
* @return perturbed hash
*/
- private static int perturb(final int hash) {
- return hash & 0x7fffffff;
+ private static int perturb(final int hash2) {
+ return hash2 & 0x7fffffff;
}
/**
@@ -251,66 +255,68 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param key key to lookup
* @return index at which key should be inserted
*/
- private int findInsertionIndex(final int key) {
- return findInsertionIndex(keys, states, key, mask);
+ private int findInsertionIndex(final int key2) {
+ return this.findInsertionIndex1(this.keys, this.states, key2, this.mask);
}
/**
* Find the index at which a key should be inserted
- * @param keys keys table
- * @param states states table
+ * @param this.keys this.keys table
+ * @param this.states this.states table
* @param key key to lookup
- * @param mask bit mask for hash values
+ * @param this.mask bit this.mask for hash this.values
* @return index at which key should be inserted
*/
- private static int findInsertionIndex(final int[] keys, final byte[] states,
- final int key, final int mask) {
- final int hash = hashOf(key);
- int index = hash & mask;
- if (states[index] == FREE) {
- return index;
- } else if (states[index] == FULL && keys[index] == key) {
- return changeIndexSign(index);
+ /*
+ private static int findInsertionIndex1(final int[] keys3, final byte[] states3,
+ final int key3, final int mask3) {
+ final int hash3 = hashOf(key3);
+ int index3 = hash3 & mask3;
+ if (states3[index3] == this.FREE) {
+ return index3;
+ } else if ((states3[index3] == this.FULL) && (keys3[index3] == key3)) {
+ return this.changeIndexSign(index3);
}
- int perturb = perturb(hash);
- int j = index;
- if (states[index] == FULL) {
+ int perturb2 = perturb(hash3);
+ int j3 = index3;
+ if (states3[index3] == this.FULL) {
while (true) {
- j = probe(perturb, j);
- index = j & mask;
- perturb >>= PERTURB_SHIFT;
+ j3 = probe(perturb2, j3);
+ index3 = j3 & mask3;
+ perturb2 >>= this.PERTURB_SHIFT;
- if (states[index] != FULL || keys[index] == key) {
+ if ((states3[index3] != this.FULL) || (keys3[index3] == key3)) {
break;
}
}
}
- if (states[index] == FREE) {
- return index;
- } else if (states[index] == FULL) {
+ if (states3[index3] == this.FREE) {
+ return index3;
+ } else if (states3[index3] == this.FULL) {
// due to the loop exit condition,
- // if (states[index] == FULL) then keys[index] == key
- return changeIndexSign(index);
+ // if (this.states[index] == this.FULL) then this.keys[index] == key
+ return this.changeIndexSign(index3);
}
- final int firstRemoved = index;
+ final int firstRemoved = index3;
while (true) {
- j = probe(perturb, j);
- index = j & mask;
+ j3 = probe(perturb2, j3);
+ index3 = j3 & mask3;
- if (states[index] == FREE) {
+ if (states3[index3] == this.FREE) {
return firstRemoved;
- } else if (states[index] == FULL && keys[index] == key) {
- return changeIndexSign(index);
+ } else if ((states3[index3] == this.FULL) && (keys3[index3] == key3)) {
+ return this.changeIndexSign(index3);
}
- perturb >>= PERTURB_SHIFT;
+ perturb2 >>= this.PERTURB_SHIFT;
}
}
+ */
/**
* Compute next probe for collision resolution
@@ -318,8 +324,8 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param j previous probe
* @return next probe
*/
- private static int probe(final int perturb, final int j) {
- return (j << 2) + j + perturb + 1;
+ private static int probe(final int perturb4, final int j4) {
+ return (j4 << 2) + j4 + perturb4 + 1;
}
/**
@@ -327,8 +333,8 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param index initial index
* @return changed index
*/
- private static int changeIndexSign(final int index) {
- return -index - 1;
+ private static int changeIndexSign(final int index5) {
+ return -index5 - 1;
}
/**
@@ -336,7 +342,7 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @return number of elements stored in the map
*/
public int size() {
- return size;
+ return this.size;
}
@@ -345,30 +351,32 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param key key to which the value is associated
* @return removed value
*/
- public double remove(final int key) {
+ /*
+ public double remove(final int key6) {
- final int hash = hashOf(key);
- int index = hash & mask;
- if (containsKey(key, index)) {
- return doRemove(index);
+ final int hash6 = hashOf(key6);
+ int index6 = hash6 & this.mask;
+ if (this.containsKey1(key6, index6)) {
+ return this.doRemove(index6);
}
- if (states[index] == FREE) {
- return missingEntries;
+ if (this.states[index6] == this.FREE) {
+ return this.missingEntries;
}
- int j = index;
- for (int perturb = perturb(hash); states[index] != FREE; perturb >>= PERTURB_SHIFT) {
- j = probe(perturb, j);
- index = j & mask;
- if (containsKey(key, index)) {
- return doRemove(index);
+ int j6 = index6;
+ for (int perturb6 = perturb6(hash6); this.states[index6] != this.FREE; perturb6 >>= this.PERTURB_SHIFT) {
+ j6 = this.probe(perturb6, j6);
+ index = j6 & this.mask;
+ if (this.containsKey1(key6, index6)) {
+ return this.doRemove(index6);
}
}
- return missingEntries;
+ return this.missingEntries;
}
+ */
/**
* Check if the tables contain an element associated with specified key
@@ -377,8 +385,8 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param index index to check
* @return true if an element is associated with key at index
*/
- private boolean containsKey(final int key, final int index) {
- return (key != 0 || states[index] == FULL) && keys[index] == key;
+ private boolean containsKey1(final int key7, final int index7) {
+ return ((key7 != 0) || (this.states[index7] == this.FULL)) && (this.keys[index7] == key7);
}
/**
@@ -386,13 +394,13 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param index index of the element to remove
* @return removed value
*/
- private double doRemove(int index) {
- keys[index] = 0;
- states[index] = REMOVED;
- final double previous = values[index];
- values[index] = missingEntries;
- --size;
- ++count;
+ private double doRemove(int index8) {
+ this.keys[index8] = 0;
+ this.states[index8] = this.REMOVED;
+ final double previous = this.values[index8];
+ this.values[index8] = this.missingEntries;
+ --this.size;
+ ++this.count;
return previous;
}
@@ -402,67 +410,69 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param value value to put in the map
* @return previous value associated with the key
*/
- public double put(final int key, final double value) {
- int index = findInsertionIndex(key);
- double previous = missingEntries;
+ /*
+ public double put(final int key9, final double value9) {
+ int index9 = this.findInsertionIndex(key9);
+ double previous9 = this.missingEntries;
boolean newMapping = true;
- if (index < 0) {
- index = changeIndexSign(index);
- previous = values[index];
+ if (index9 < 0) {
+ index9 = this.changeIndexSign(index9);
+ previous9 = this.values[index9];
newMapping = false;
}
- keys[index] = key;
- states[index] = FULL;
- values[index] = value;
+ this.keys[index9] = key9;
+ this.states[index9] = this.FULL;
+ this.values[index9] = value9;
if (newMapping) {
- ++size;
- if (shouldGrowTable()) {
- growTable();
+ ++this.size;
+ if (this.shouldGrowTable()) {
+ this.growTable();
}
- ++count;
+ ++this.count;
}
- return previous;
+ return previous9;
}
+ */
/**
* Grow the tables.
*/
private void growTable() {
- final int oldLength = states.length;
- final int[] oldKeys = keys;
- final double[] oldValues = values;
- final byte[] oldStates = states;
+ final int oldLength = this.states.length;
+ final int[] oldKeys = this.keys;
+ final double[] oldValues = this.values;
+ final byte[] oldStates = this.states;
- final int newLength = RESIZE_MULTIPLIER * oldLength;
+ final int newLength = this.RESIZE_MULTIPLIER * oldLength;
final int[] newKeys = new int[newLength];
final double[] newValues = new double[newLength];
final byte[] newStates = new byte[newLength];
final int newMask = newLength - 1;
- for (int i = 0; i < oldLength; ++i) {
- if (oldStates[i] == FULL) {
- final int key = oldKeys[i];
- final int index = findInsertionIndex(newKeys, newStates, key, newMask);
- newKeys[index] = key;
- newValues[index] = oldValues[i];
- newStates[index] = FULL;
+ for (int i11 = 0; i11 < oldLength; ++i11) {
+ if (oldStates[i11] == this.FULL) {
+ final int key11 = oldKeys[i11];
+ final int index11 = this.findInsertionIndex1(newKeys, newStates, key11, newMask);
+ newKeys[index11] = key11;
+ newValues[index11] = oldValues[i11];
+ newStates[index11] = this.FULL;
}
}
- mask = newMask;
- keys = newKeys;
- values = newValues;
- states = newStates;
+ this.mask = newMask;
+ this.keys = newKeys;
+ this.values = newValues;
+ this.states = newStates;
}
/**
- * Check if tables should grow due to increased size.
+ * Check if tables should grow due to increased this.size.
* @return true if tables should grow
*/
private boolean shouldGrowTable() {
- return size > (mask + 1) * LOAD_FACTOR;
+ return this.size > ((this.mask + 1) * this.LOAD_FACTOR);
}
/**
@@ -470,16 +480,18 @@ public class OpenIntToDoubleHashMap implements Serializable {
* @param key key to hash
* @return hash value of the key
*/
- private static int hashOf(final int key) {
- final int h = key ^ ((key >>> 20) ^ (key >>> 12));
- return h ^ (h >>> 7) ^ (h >>> 4);
+ /*
+ private static int hashOf(final int key12) {
+ final int h12 = key12 ^ ((key12 >>> 20) ^ (key12 >>> 12));
+ return h12 ^ (h12 >>> 7) ^ (h12 >>> 4);
}
+ */
/** Iterator class for the map. */
public class Iterator {
- /** Reference modification count. */
+ /** Reference modification this.count. */
private final int referenceCount;
/** Index of current element. */
@@ -493,13 +505,13 @@ public class OpenIntToDoubleHashMap implements Serializable {
*/
private Iterator() {
- // preserve the modification count of the map to detect concurrent modifications later
- referenceCount = count;
+ // preserve the modification this.count of the map to detect concurrent modifications later
+ this.referenceCount = this.count;
- // initialize current index
- next = -1;
+ // initialize this.current index
+ this.next = -1;
try {
- advance();
+ this.advance();
} catch (NoSuchElementException nsee) { // NOPMD
// ignored
}
@@ -507,45 +519,45 @@ public class OpenIntToDoubleHashMap implements Serializable {
}
/**
- * Check if there is a next element in the map.
- * @return true if there is a next element
+ * Check if there is a this.next element in the map.
+ * @return true if there is a this.next element
*/
public boolean hasNext() {
- return next >= 0;
+ return this.next >= 0;
}
/**
- * Get the key of current entry.
- * @return key of current entry
+ * Get the key of this.current entry.
+ * @return key of this.current entry
* @exception ConcurrentModificationException if the map is modified during iteration
* @exception NoSuchElementException if there is no element left in the map
*/
public int key()
throws ConcurrentModificationException, NoSuchElementException {
- if (referenceCount != count) {
+ if (this.referenceCount != this.count) {
throw new ConcurrentModificationException();
}
- if (current < 0) {
+ if (this.current < 0) {
throw new NoSuchElementException();
}
- return keys[current];
+ return this.keys[this.current];
}
/**
- * Get the value of current entry.
- * @return value of current entry
+ * Get the value of this.current entry.
+ * @return value of this.current entry
* @exception ConcurrentModificationException if the map is modified during iteration
* @exception NoSuchElementException if there is no element left in the map
*/
public double value()
throws ConcurrentModificationException, NoSuchElementException {
- if (referenceCount != count) {
+ if (this.referenceCount != this.count) {
throw new ConcurrentModificationException();
}
- if (current < 0) {
+ if (this.current < 0) {
throw new NoSuchElementException();
}
- return values[current];
+ return this.values[this.current];
}
/**
@@ -556,21 +568,21 @@ public class OpenIntToDoubleHashMap implements Serializable {
public void advance()
throws ConcurrentModificationException, NoSuchElementException {
- if (referenceCount != count) {
+ if (this.referenceCount != this.count) {
throw new ConcurrentModificationException();
}
// advance on step
- current = next;
+ this.current = this.next;
- // prepare next step
+ // prepare this.next step
try {
- while (states[++next] != FULL) { // NOPMD
+ while (this.states[++this.next] != this.FULL) { // NOPMD
// nothing to do
}
} catch (ArrayIndexOutOfBoundsException e) {
- next = -2;
- if (current < 0) {
+ this.next = -2;
+ if (this.current < 0) {
throw new NoSuchElementException();
}
}
@@ -589,7 +601,7 @@ public class OpenIntToDoubleHashMap implements Serializable {
private void readObject(final ObjectInputStream stream)
throws IOException, ClassNotFoundException {
stream.defaultReadObject();
- count = 0;
+ this.count = 0;
}
diff --git a/Tests/arrays1.class b/Tests/arrays1.class
index df1e9ac357781be2475b93cb342a24fafc25d9bb..e8cb0ee4d5abe69aa4dc80fec8a2c97d842714a4 100644
GIT binary patch
literal 2569
zcmbtV>u*za7=BKB+S7L3m30i;!2t$t1v)?+47xF{I@uU7K)DDz?Kv9<x}N2nQ*d|-
zh@gpyN;Ki3iJ%D|yhJe>M9BE235oxKe}akM5zyy%PDh8JUu@Ig_5Ho?^FHsTcOU*V
z1z;75G0a0(3@unIhIL}dMmcmV=!sx`3}N&}upx$x*c8QPY*DZ^hB&$+ctOlBilHxp
zmm=5}LBH4y#IPNM5$uRyr_i@cD53n2INvRXJqq^5@G@ReuusCQR?Tq?+cmACv)OdC
zT*1&KNc$y(vu4qBdn5$g+V@J3H(9zNp|;;F8rw@_Im6y9gn2QhnMDarZ3p^~YR9#X
zf>s>u7;<g1IJ!<eR7T9AJ|ILwZ3p_=`y^Bkxmy0%fHq#%5Y1`&F2gZTQd^iZeeHV{
z5J7CzvL0P1-o*hvuNMk86!jf6;qK5(+o5Q#lp`9)vfZ*BT8=nJtP}mF!=ozG+2G`j
zqE1w00UC&8^M$gLu_3Eu=Z&qVa4D|Ywl?9c$OwnxSb&9bEXUF~R$yfu&xt|Bd<o4J
zhc`^KxW%?Do22d7wMD!<K#E5+YSq<o+sIo)Ah=d=FpgJoNWtMahM`HAUD4%}x3Odv
zbc3o=yN?*Ed%{wUf-z<kT}Rbil@yqH!%^eNAuk3-Eu?BiUG-+$;9R9@x~`VSRo9}N
zfe{6xaU6lkFcvIpT+LghqHEZyMd5nWQLU1zS|e(X$GVe=Gew_gF7WM9nBw6=Mzc(f
zf@5(MFeag{0(>xc)X0<VfCy8fZAL!$H(ox}ROAOV_Xw#P^OJ*d=d&5=h9(@>poJiD
zQJ=5Qv^u=NlO#hMTgQyi#>W|03Cm_0oKC<Q7#^dQ4^wS@?f-EdaV`IagvPcf1*u?`
z=gH%M$k4dR%L4QLF$SgqF)u@&1cOjvVpD--$Rg5N2DYI;$|hEdTjB+4a6jg=p69W1
zNOjF3|G0`l64}YImAe+s66a9*2BaT^AQo{9dxv2}u^7*CEkxf%fM1}iPPrZHUlO^A
zz>=E?@+a3-iIb;o<QW$g^=nZ>MG=IECWb2Rs?mU2%tjrOs3+oCG}(wYB(RjH%hAll
znu9gGjq<d;3~2&Eeu2*G2wg%``e#JaQ=g;y7Q*`)lpBcL31;Q)RC?+v8q=vvI+?kO
zP%3*SAYJ?G_vANx8Svbl3x(_Xw6KsCS~)JF-Nndoy$Wf5L4={&=mP{LsqP+uN3nz=
zJ~L+_^91PjU?d1bNq$yF5fvzsw_^k8spL(>dV-yDLT<T=`lSguosctwXJmr;W9c@*
zj*n&mnGwCd8J$RBHPLj@)LNc&aa@lqdObw7kZYn3QLSK^B;6xrQ3CELV>(sFl>Hx=
zzJCPCC#a8*wh>Z4A#Eq5K|<P2NW1<G4jW(@&aZ?cQ{CGhoci=HGwBKXAu>|(a8HW}
z)*cb8mdtSS3v9lQs#}QfyMgM4nn~2ACQ;W=&qa$^G;l%L=`+3&%UL{4axsa<NhHn$
zN$}TR%rF0w<bzDIL-gn{gFVbvt-<E{HJ-hN5znhegd6WelI|la{fV6ny&rwHb>B59
zS!VjXr@1C~2Yr{`OkKo8u-glNda6a2^{dExFIFbx%ZMjrc{n|F1+5}?ryXvhBMDi!
zG@C2BBa%sE4S(`*<|`!SZhx8eCUG^$A?at;1<&<&JSz?9n`piyxD1oaId>{d^sw*%
zi%i&Pg2U$EGVM$B?>I)ug^LNUPU20xj&pbeAMoxx<u2e9zQt*erP+u!K4d8ho@%7I
zYOBvvBU6%pedQb&B~hY*EDvUrBFe3m(6Taxm(TcKP9k|mV$go0z$8)?s7+p(on?KT
zV+x*SA9#-m|GozyioksYSO<$~l>b6yqo>O)V!g~xki3XBUN>0jags<~MwI(26<X3M
zS<f(|zJwxQgB<jG#oZ@*#fS9dBl`0(d)IlI{DgJ-DY{9D-z&loAWPC5rKVR36K*Hr
n`n_TmXYr|TU;@v*R5tS?LKQEko3GFmLLlBNTJ&me0$B4m*_8}4
literal 9377
zcmcIq3v`rKlK$@Bo$gL|hul9&Cm|0E2nqobMdd975fp*&2=Z2F=mvsGI;IoA$LQ!V
zqpokq7tKm{67+Y}Rm2tWg|6eM<M<d?N1fTn?4CKZ=ggclyR&=7v(604R@LplyA#ma
zv*#@7$E~_mb*t)rx9<IK^UhZ<9tUt9_5{&@S;d%*3xo7ACx}s)%O5TLF|U|DF7ji3
z02c=lz=9wa;*w%qibZ~07DNeV1+bXEm+;5Z09pfB7Qk|*Rs^vUZ2_zb;Bq#$nk|t0
z8s@L%k9B^m4`Ks0`f-Iq`PgVO8Sm+BPjn?OZcj$Hbi`u{YQ2JQc6(QQ?;His_z9~O
zyz>*WxI*cY_O5tqU+0#1&ngzCj?QR%mqO+E4NG=LcSV~!qFvjY+j@K2ySC3_#gew(
z=+>*2M!QAck1PGyq~PDy-W6NQibdl$ESj)Lp?FI)wlbb<zm{zJh_{H9gWD5{9M>=0
z4J2!`_PnmxavG&~d9=MJNupc&wva=~L{D$lDCq~1I}*E>v?qxbYERBfZjE=v$g!*d
zMH!gAwIds6ur1Novo*f3oudjzdwQbRB+qT)n8G*{WBu41Mig7Z*os&fQ_viysXRZ7
z3;1I+#wb+h6EM%s>Vlr0L=WY8Ta@g^8oGPpTNC61C!Ed3{n!@9cI@z@J&c{WN}(!m
z#ia3~zV?n-oQ%}1+7WN)-JNKNcf>p6UA@VMXm0~$qJ3*T*$_qtI{AZh+7RuEHOO~Q
zoW4U1(O9gZue+f)L2?On`*C#`J)pFeb|ezr4O<g^UA^(1h6D-Q?a78jUvEQVTf-J&
z$C6E9OvN-p1?l!8$%<oX2D2IRqc4nI*sY-RjxXD?GrpCQZt-lDp9UEUk<RGOL{D>P
zUvHF?(L6uVwXL0I#<ywH(oL<)XgE^!&tJBB!O8^}^Mny1Xu=}n3t(o35txn0556?o
zyMticY0yP#WT?Qmwri5T@lFz;AjzIF*Pdt=Fj2<i(au@qMzp(|z@jj@a6lK=1wIU!
zBT}pzzi7fYbO(A9Mnj=u{HcOupj;vu>JVk3o3Y+OlRG2>u0w?NB9WjO&1YhM2d!>e
zn=x8fJ@Hr$l(Zy!`>2DK_IiTuC@M#Q($x%OY6YPf@$@;4sCxQV^j*|=6zW+P#98#|
z6Q&QvI2+@sO`_IE@W7()a}UExL3@ji!Lttm?RQW|tfCCH|L8zd+na&k<Df|UUk)xI
zI*`U((Fz3uq?N+C6NN1G`NfDo;GmW`ezx&v2c^{Z85>?w@DizgX;g_)iS}uqSn*Fh
zh9d6s=llGcO{TzoKJE*qu`sI_)IsT+Ds-6+=wcZ@phFHuv2Zav@VNt<iGUkL$V8z-
z`C&pjlp97|2<Q94I-Khh7fSOkl<LwUE|lmI!(13q=t9YG7j%9Yt#xh~aly{_+1k$a
zi3=5J%+F?_LRU!Nc|zN|OqYubey^EGT~32qW+HW2b{4$Z6h!i4M06xKhKygC@2k|6
zxjrAm$`V-3#0Y8!&`c=oK?rxzruGC%@j0}zVXMg~S9?&Q?ngu&LY4Xg)m8;YTIZk^
z6G(G8CY6VR^VA7c`O&zN-izsd8NE;P7=BEoCVw|7tI9)v72(jlQ=8?XP>bObz$amH
z7T~`ofP2Wys>AT76k|{~WDsgRegI!MILY)G83Y^O#BUt@p2<-e_#FHLH|sN~qaIG8
z*TX8NmBA|x-XMV#M(TRqAek;D!N*vp-@)UoTqSlGfhknzDqSUFJkpI0{PeYlrRqeg
zlbf~T*M4kvu$}1|q4#0AgEe9$qHA=WSP}oHJDA&eTzYI>tw%}^FHv5(dSt<bS5sSJ
z7(~fS2&^kBK8oP0S<TUU%uvlS1)8H>&DmM$Gxb;_?E-6Tf%KWwrt!Vr3)zFSCA62h
zc~%DDy2j&!c-jF&RF5-^G#+s<Mod@gar$gA&5{Gy>!4T~*Rgz~*xJd>2^o|&)-^TO
zHVtB(19nW0&+*b&;9$I19I40aMzNTcAHW0$VWT^MdRCm6Mnr^5^h8b7g^Em3-R!-V
za!#7!X6s3Ml8Kli<2tA(WuvTpit#CHU<~0O7_G{1rfQ+RwhKP>BF0%|ILn%ZvDOqq
zFk^iUnkz>HOIy^XiovY}*-91F1}i<m($cES)nfW9?6Qgl*e7TKF~CodQc&yaqF{M>
zZJ<j12}R|^CdfC@0yH)KDR@yto|OsY1MKotf_UwI{Fj42GI@bP{I4ARmdW!axj*CP
zc^TB^5KkH|;Ey>lc&XOs>8X;B5hT}7A~b^sS#`2laq&J`PZlZ0`*jBIy(~3Fq>|h`
zmz_F*D;&g_Jcr2?S{+<YB(Irs^b})*Mw#Yd4(}!@*t$tK=VnB(-dupeCTa`T2Tp_a
zX?mK`R1PRTmYzn^)b`cB99){UK3z}GS!ZnM>1Mu*8;{o>LugJ`Y=)kh6B8$97C14(
zbz-WQEnJvK?`#5o#9KdzjoFnj%P`VdoL>pE^o3%ZB?mBtR)RDpu&p_1*;P|0(R1`1
z5=$X8DdKI6c$=2(^%8FHWvRJ&T+h{WMXG4h;(XCQix2~xuR@rrn(3&x8Z*>)3A7(#
zrut86|2O7ZHd+L<8!<5=puI$pDU}!&p|*xmJ7PrTsvK%_eGJ=+2;GER`V1`~;JN@-
z2EbK*!fq8K_Z*y?MecK1<c`cEchOMfUOE)Hm*kPV@Gm2Gp<X0u9gf_VA;@jfEh04>
zxeM~hy?7{c=bwVy`Feq|F$}r$^hLtYRq2ZgKr_z;&FPSPnZC?uy2!nZq=zAQv0j|B
zF34R>GE}vOA$N&hniCV`E-i3kiR*+x?(#fxmkmd5>uHeNs+WuH(;;_79=R*@3KBaV
za(R8P)GLjH6rWVwl_pm2q(cPS!iu|y0KAw0yo3PUng#GO0&pt<c%^`MGba6iftLy|
z*Y9G`lcfQ$X9@w>OD+yDfXz<VCK)t4QiX2QZ4w%TD@aGu#<xyWrB><7P5d->GC`LY
zOwcNKf@F_f%hs(6c*(D!>EJ!qIy+lgRvSjzs?1lG)q1U%mOWN|ncZX6AK1W^8QO8Z
z9S(Y!x<aT}wm5GTYKMc>+_yofZU>hVl|s4Rpsy6Oq)(@pDeN>)<T}0H1VRN_0$E=W
z$U16MfL`xrE~z@ok*GK~H<RP_6p31sjbxKyq}9TFB%5^9L_(4SYBEJ4jj?QChuA9T
z=JpIFnNAD!O`B``6|#HPwgT=Te(T^al1-sjZ__)(YECDEcO7)IrFaG<#uBAyJ#%6?
z4yB1xp||EZlq!BA(OYsHN*6nqLY3a4<1$Lt9;Gbk`k28+R%=g#POKzcqT6*l38!%J
zVT4~o$-1K$QC4~cy6y<<vNCGabEBLZWW(iAyxgoHZY?#AAaVqidp*ke>Onr-eEDX6
zD`=#1JFt;%46a0s9ug1HZBG+z1=nJ;H5*au0c^7N<4UU^+hj$xVzOQ7agQb0<46hp
zi{$qK4=oHumkCN09$6xhdYk@@T&O%%e?|+{e|pjSp-UOFeu5tmO-C31V1E7V9I}3P
z>Yb9gZ(KiD>8nJD&jC_Du5zKqYleZ@p*xL)yTUpPfZ0K9()4-+m%UWn>-PD+a_|^W
zOwvGc!1p@`4=|&L{qy~jn^$KLVGw53>oUH#4R%tf(O2tU8B()^?-?@rq=PnA>lO=-
za5IrbzVGfV^1HIg_uY_3ewXeROT0z~eDN&ueH+Q-S~jvP4K4_bon3ktiKZ}4Xj}K`
zzFgdrnLamGH#58So}7d%**yiB+3iZp=3wKy?0L~Yk#QS)X-UyB<am9|8yhV8v7>lQ
z8{a8lr;83dYJ|8_Pd%hBL*>*4itcmp?-8#k-b|5;HCk<-3g;%5L+j;7!uht#q1E;r
zarBKYgBBarU|DQ8+PGQ9G3IEg-pZoa^GV`(Jy~DO<aLH5)3cep){ta(GLzRBlB~Mt
z+iUdoVw7!=Nk4y)B!lZ)`UaCi0+FQfhJqA+i`r84VgufTjB?9_`w%_BM5q>WG5gR_
z|3S8FJV;M~5$}HWnxp<%7!Pp5)w9yRKZDWKnFU)`H%n#IosN1^{AsXpzm12)qY5^b
zbcfmLD9(h9zhbNCllE;g<N>wR6n-1G3L~Xv8?;jSA|C08LGf;kgBdbuv=i9)o{d{f
z_!K5*i)a%+-@j15i=lq}Mi}3h(G7_1%Vl8@KXI}G_vV;s9C7e5X;G=Raj%W<%SdkG
z@UVj;V)GuFFA9?;_uE3>ZD^V(F6B1vGBi!^W})viG|lgFqEo1}ai@)Y#5x-ySWL@@
zc)N`|Oo%kYCd4}mL%iLcW17u=jO8b8w{TZcL5_I2G*?rL%5wHW+(w4eVBIe6q%$bz
z13kUHo16NrJ`=T#14BB}7Cl6~Bo3cJePlztDo{OW&2+F&Oo`z~hUMk2hvjAeu)L&B
z%}dJ0BVUu3hi&W|mY02nd3iXOm!^ZNUmO}pW2OX9YGZ(2q@Kz?z7v-E>6J5R;M4Eg
zxUf+SJU%QUXIMm!4U6c}QzLrR#^YZT(V&fkIS0&4A1sV$(Di0>6PFDe&!pw@Ck2Y<
z8G1=P4;ojW9_H%b40H9VVXi)Ts;f`hc=~Hx{eg`qhPnDgp{qa0xyo=@Cf*)OqsGnt
zAsdIp+W_^~%A@3;>iNX*#R=Jr%NmbiB%Rn9%|}u5YW@JR5H=kk5_Ev*!CEBoJvuy0
zN3ZHZpX!It`Zw(I{tkPJeuZm%XX0AlbGXhQ#r6K1(C5DeN&lU=$v=Rb`EX&qkK4@Q
zqD6g)3gqrQM(Cj3qI`97_u;9MJCE$eh*F`-$}`&33i?~F)~VL)-)eeV^`MB4=*pZ$
zPNIAm9r_D2-J!es9x`&0;><DVaAVcz5V^JFl#Ze?A+1NQp`KIwtWZToeJTB`K7D_S
z@-~F3t4E)t_zMOjKTguE>i>mPeTr69p5swunF0v^uUG}~dqr_*=*F0*CK7H@SWbqQ
z6};C<2n9pSZNZR{zm`)lt~px{oeC2|orFO1r0|V{i^PzjzL{eN7nz}h=heJ5C;9Gz
z{1C9goNX)Ua7#Znn!~MXBngWU^slnysJuOE<FHw>xvlbW;gWrp2-;!19#dPMmyL3-
ztlYn)gHA19sM6NJ&lxtJGn_QGy3ZNa#I*6ejKIPJxRlO{(%`#I8%NSOM|`1Tb%b8B
z{He;hj~R5u$~zT3K=4j=1a*5A-7oDD-J|ZqJn0^#m*^Ig?h(}IOG6DkPk;)-6#D)S
zZov!GeigUkUvQf|OH`q>GE7)GLD!lg+pa09siDl(@IwLpfNApPeUI|y0X(mWuaviA
z^fGy)?3iugm|NXARdNn_!N!X@Ayc|vEKKeTt_GicZTuajkFT3O7dUuYIImIpt=;Dt
z=iq?QuX6f5mC`;=C;eKvoi-DcvFQ0=H+7{@XX7}Tlc9C(KI_*kX8qE^S|UCZ?N?;0
ze^=Tsn{fxNSKNtw$#BvZJs*q}lQfYp*?2`vij&qo*#~#)7Ou@|p_qCv8-i+f)cL}B
zmqMu9ug-838?x~e9$4|g-^M!`)YrME$HGwXdk3GBh=lTvjrU9_B>Sm|edyp5vGAtg
z@oH)Rh(|hr=N&|aeuL>09(AxnOwobr4I6KYDRK#SIGA21Jv5)M+xVgM@X6Rr)ej4&
z>UAPy9rVjXv5g<g$o#}@<Lzt$F@tW1h4WT6fuM_!Niqf{@Ga8HClFx*4n@<S-_Jz#
z)3mA(4MO#&^dgOvvZU)1<HR3?_*n*(jdk8w6FqVp{y&oIW_CX==rfOkuTkI2Vs?y;
zk8OM+j^qpsN_6{4=pl1Z_{hD8;h#Qi{JoHy9dro!p?ei`g^)jW?_yeIgourw+W1ID
zpxc-jp(>Z>_icP29h^;*=MM_={5}!nh1bMo+;WT0XXz8akO3$&pV5mmbK-5jOE~em
z@M#`@PA_AhteAEA^Q_5&-%3WoPc`9g`uX`D`aR@cRe}4gD{#MOHy-djjEAKz`~nLr
zr7Tn`w>;RTp*GoUObM0?=uxFyGpb5Mx`qDl0dEO~ogvy{SLe3ie2*oS#$OZWUlSWV
zyhXJZyw_0sBr0>Jh?MQoHE?=5H?$Ee^o13Iv>(<K$+j54^xQA?7f^}ge`Vzubp&V7
fFWiFj=itxRQ1@qhIv&y8h*d(C6lM@%Vdnn;iiyJx
diff --git a/Tests/arrays1.java b/Tests/arrays1.java
index b2a09fd..4fdd4d0 100644
--- a/Tests/arrays1.java
+++ b/Tests/arrays1.java
@@ -30,7 +30,7 @@ public class arrays1
// pre: list != null, list.length > 0
// post: return index of minimum element of array
public static int findMin(int[] list2)
- { assert (list2 != null) && (list2.length > 0) : "failed precondition";
+ { assert (list2 != null) && (list2.length > 0) : "PRE";
int indexOfMin = 0;
for(int k = 1; k < list2.length; k++)
diff --git a/Verifier.hs b/Verifier.hs
index 73f6e84..629dcae 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -105,6 +105,7 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
PrimType FloatT -> mkRealVar symbol
PrimType DoubleT -> mkRealVar symbol
PrimType IntT -> mkIntVar symbol
+ PrimType ByteT -> mkIntVar symbol
RefType _ -> mkIntVar symbol
t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
@@ -141,17 +142,20 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ast2 <- e2 env decls
mkSub [ast1, ast2]
LShift -> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkBvshl ast1 ast2
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvshl ast1 ast2
+ mkBv2int astr True
RShift -> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkBvashr ast1 ast2
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvashr ast1 ast2
+ mkBv2int astr True
RRShift -> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkBvlshr ast1 ast2
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvlshr ast1 ast2
+ mkBv2int astr True
LThan -> do
ast1 <- e1 env decls
ast2 <- e2 env decls
@@ -178,17 +182,20 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
eq <- mkEq ast1 ast2
mkNot eq
And-> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkAnd [ast1, ast2]
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvand ast1 ast2
+ mkBv2int astr True
Or -> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkOr [ast1, ast2]
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvor ast1 ast2
+ mkBv2int astr True
Xor -> do
- ast1 <- e1 env decls
- ast2 <- e2 env decls
- mkXor ast1 ast2
+ ast1 <- e1 env decls >>= mkInt2bv 8
+ ast2 <- e2 env decls >>= mkInt2bv 8
+ astr <- mkBvxor ast1 ast2
+ mkBv2int astr True
CAnd -> do
ast1 <- e1 env decls
ast2 <- e2 env decls
--
GitLab