Fixed unsupported type int[] as variable type

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -182,4 +182,4 @@ EXE_MARKER: '\u2316' -> channel(HIDDEN);
 
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' )* ;
+ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]')* ;

src/main/java/edu/kit/formal/interpreter/Interpreter.java

@@ -36,6 +36,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
                     .put(Type.TERM, VariableAssignments.VarType.FORMULA) //TODO: parametrisierte Terms
                     .put(Type.INT, VariableAssignments.VarType.INT)
                     .put(Type.STRING, VariableAssignments.VarType.OBJECT)
+                    .put(Type.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
                     .build();
     private static Logger logger = Logger.getLogger("interpreter");
     //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)

src/test/resources/edu/kit/formal/interpreter/paperExample/Simple.java

+
+public class Simple {
+    /*@ public invariant log != null && log.length == 100; @*/
+    public int[] log = new int[100];
+
+    /*@ public invariant n >= 0; @*/
+    public int n;
+  
+  /*@ public normal_behavior
+  @	requires log != null;
+  @	ensures n == 0 && log != null;
+  @*/
+
+    public void init() {
+        for (int i = 0; i < log.length; i++) {
+            log[i] = 0;
+        }
+        n = 0;
+    }
+
+    /*@ public normal_behavior
+      @	requires n < 100;
+      @	ensures log[n] == x+y;
+      @ assignable log.*;
+      @*/
+    public void logging(int x, int y) {
+        if (n < 100) {
+            log[n] = x + y;
+        }
+
+    }
+
+    /*@ public normal_behavior
+      @	requires x >= 0 && y >= 0 && n <100;
+      @	ensures \result >=0;
+      @ assignable log.*;
+      @*/
+    public int example(int x, int y) {
+
+
+        if (log[n] == 0) {
+            logging(x, y);
+            return x + y;
+        } else {
+            return x + y;
+        }
+
+    }
+    /*@ public normal_behavior
+      @	requires a != null && b != null && (\forall int i; 0 <= i < a.length; a[i] != b[i]);
+      @	ensures (\forall int i; 0 <= i < a.length; a[i] != b[i]) && \old(a) == \result;
+      @*/
+
+    public int[] compare(int[] a, int[] b){
+
+        return a;
+    }
+}
\ No newline at end of file

src/test/resources/edu/kit/formal/interpreter/paperExample/test.kps

+
+script t1(){
+    symbex;
+    cases{
+	    case match `a[i] >= 0 ==> ` using[a:int[], i:int]:{
+            auto;
+	    }
+	    default{
+	        auto;
+	    }
+    }
+}
+
+script t(){
+    auto;
+}
+