diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index b380bfe34d585856a033e10491359d51fc37509f..3580e2ae1d4b10c24444423ebb200c2a243650a6 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 0000000000000000000000000000000000000000..d0c78646721a8fb920fee02ff787f1a484f38d1d
--- /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 0000000000000000000000000000000000000000..a4cce7ea4bacbe5964a2e2cac6ebcceb0d587e96
--- /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 0000000000000000000000000000000000000000..5f12fa9d40a19e07e3ec668b7d38efc1447e690a
--- /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 0000000000000000000000000000000000000000..b4b5559ab0c0a81a9fd9a5974fcba48959b9f715
--- /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 0000000000000000000000000000000000000000..179bdce427c8f3960cfa5fa328d8a177ae9dbbeb
--- /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 0000000000000000000000000000000000000000..57ea17611731a00ec1ad3a11fe9e9c02842af947
--- /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 b241d710a6eb7fa53efa75b09359d9f6e58e8db2..d2469778eae57064514c4dcf15563666368a82d9 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
Binary files /dev/null and b/Tests/GradientFunction.class differ
diff --git a/Tests/GradientFunction.java b/Tests/GradientFunction.java
index 25aa7c79892ef0d824a3df877986cf9bba6a831a..c85f6cf296860f03ab040806233bdee25e6dadf7 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
Binary files /dev/null and b/Tests/Iterator.class differ
diff --git a/Tests/Iterator.java b/Tests/Iterator.java
new file mode 100644
index 0000000000000000000000000000000000000000..eda7b854d3e20ac3cb485d27644c0c831fbe582c
--- /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 9fb3e0aa8b5c90ef5d52397617d6cd73d66c5f84..03fa6489d1e4cd738677897d1e297fce087b9603 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
Binary files a/Tests/arrays1.class and b/Tests/arrays1.class differ
diff --git a/Tests/arrays1.java b/Tests/arrays1.java
index b2a09fda2eac3f423ea5b4531460998a1df3dd03..4fdd4d0b5f04fd68b1295d5fc1d10331fd8411ae 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 73f6e84e081f52850b603f625358e288360ce015..629dcae1bf8cd7ca273e6f2fbca4875d61391fca 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