more array examples

Settings.hs

 module Settings where
 
 testFile, postCond :: String
-testFile = "arrays1"
+testFile = "arrays3"
 postCond = "(true)"
 
 nrOfUnroll :: Int

Tests/arrays2.java

+//https://www.tutorialspoint.com/java/java_arrays.htm
+
+public class TestArray {
+
+   public static void main(String[] args) {
+      double[] myList = new double[4];
+      myList[0] = 1.9;
+      myList[1] = 2.9;
+      myList[2] = 3.4;
+      myList[3] = 3.5;
+
+      // Print all the array elements
+      for (int i = 0; i < myList.length; i++) {
+         System.out.println(myList[i] + " ");
+      }
+     
+      // Summing all elements
+      double total = 0;
+      for (int j = 0; j < myList.length; j++) {
+         total += myList[j];
+      }
+      System.out.println("Total is " + total);
+      
+      // Finding the largest element
+      double max = myList[0];
+      for (int k = 1; k < myList.length; k++) {
+         if (myList[k] > max) max = myList[k];
+      }
+      System.out.println("Max is " + max);  
+   }
+}
\ No newline at end of file

Tests/arrays3.java

+//https://examples.javacodegeeks.com/java-basics/arrays-java-basics/java-string-array-example/
+
+package com.javacodegeeks.javabasics.stringarray;
+
+public class JavaStringArrayExample {
+
+	public static void main(String args[]) {
+
+		// declare a string array with initial size
+		String[] schoolbag = new String[4];
+
+		// add elements to the array
+		schoolbag[0] = "Books";
+		schoolbag[1] = "Pens";
+		schoolbag[2] = "Pencils";
+		schoolbag[3] = "Notebooks";
+
+		// this will cause ArrayIndexOutOfBoundsException
+		// schoolbag[4] = "Notebooks";
+
+		// declare a string array with no initial size
+		// String[] schoolbag;
+
+		// declare string array and initialize with values in one step
+		String[] schoolbag2 = new String[4];
+		schoolbag2[0] = "Books";
+		schoolbag2[1] = "Pens";
+		schoolbag2[2] = "Pencils";
+		schoolbag2[3] = "Notebooks";
+
+		// print the third element of the string array
+		System.out.println("The third element is: " + schoolbag2[2]);
+
+		// iterate all the elements of the array
+		int size = schoolbag2.length;
+		System.out.println("The size of array is: " + size);
+		for (int i = 0; i < size; i++) {
+			System.out.println("Index[" + i + "] = " + schoolbag2[i]);
+		}
+
+	}
+
+}
\ No newline at end of file

WLP.hs

@@ -87,6 +87,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
                                                                 -- We don't initialize ref types to null, because we want to keep pointer information
                                                                 RefType _ -> acc inh 
     wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e)))  = snd (foldExp wlpExpAlgebra (Assign (NameLhs (Name [ident])) EqualA e) inh)
+    wlpDeclAssignment _ _ _ = error "ArrayCreateInit is not supported"
               
     -- Unrolls a while-loop a finite amount of times
     unrollLoop :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
@@ -159,7 +160,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
                                                                     in  (ExpName var, (substVar (env inh) (decls inh) (NameLhs var) (InstanceCreation typeArgs t [ExpName (Name [Ident "#"])] mBody) . snd ((fMethodInv invocation) inh {acc = id}) . acc inh))
     fQualInstanceCreation e typeArgs t args mBody inh   = error "fQualInstanceCreation"
     fArrayCreate t dimLengths dim inh                   = (ArrayCreate t (map (\e -> fst (e inh)) dimLengths) dim, acc inh)
-    fArrayCreateInit t dim init inh                     = (ArrayCreateInit t dim init, acc inh)
+    fArrayCreateInit t dim init inh                     = error "ArrayCreateInit" -- (ArrayCreateInit t dim init, acc inh)
     fFieldAccess fieldAccess inh                        = (ExpName (foldFieldAccess inh fieldAccess), (acc inh))
     fMethodInv invocation inh                           = case invocation of
                                                             MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function