Support for function invocations as If conditions

latte/src/main/java/typechecking/LatteTypeChecker.java

@@ -522,6 +522,8 @@ public void visitCtIf(CtIf ifElement) {
 			visitCtVariableRead((CtVariableRead<?>)condition);
 		} else if (condition instanceof CtFieldRead){
 			visitCtFieldRead((CtFieldRead<?>)condition);
+		} else if (condition instanceof CtInvocation) {
+			visitCtInvocation((CtInvocation<?>) condition);
 		} else {
 			logError("Cannot evaluate the condition of the if statement: " + condition.toString(), condition);
 		}

latte/src/test/examples/MyNodeIfInvocationPermission.java

@@ -0,0 +1,44 @@
+package latte;
+
+import specification.Free;
+import specification.Unique;
+import specification.Shared;
+
+/*
+ * This file is part of the Latte test suite.
+ */
+class MyNode {
+
+    @Unique Object value;
+    @Unique Node next;
+
+    /**
+     * Constructor for the Node class using @Free value and next nodes
+     * @param value
+     * @param next
+     */
+    public MyNode (@Free Object value, @Free Node next) {
+        this.value = value;
+        this.next = next;
+    }
+
+    public @Unique Object test(@Free Object v1, @Free Object v2, @Free Node n1, boolean c1){
+        @Shared MyNode n = new MyNode(v1, n1);
+        Object o1 = new Object();
+        Node n2 = new Node();
+
+        if (this.test(n, o1, n2)) {
+            this.value = v2;
+        } else {
+            this.value = v2;
+        }
+        return this.value;
+    }
+
+    public boolean test2(@Shared MyNode node, @Free Object o, @Free Node next){
+        @Free MyNode mn = new MyNode(o, next);
+        node = mn;
+
+        return node == this;
+    }
+}

latte/src/test/examples/MyNodeInvocationIf.java

@@ -0,0 +1,35 @@
+package latte;
+
+import specification.Free;
+import specification.Unique;
+
+/*
+ * This file is part of the Latte test suite.
+ */
+class MyNode {
+
+    @Unique Object value;
+    @Unique Node next;
+
+    /**
+     * Constructor for the Node class using @Free value and next nodes
+     * @param value
+     * @param next
+     */
+    public MyNode (@Free Object value, @Free Node next) {
+        this.value = value;
+        this.next = next;
+    }
+
+    public void test(@Free Object v1, boolean c1){
+        if (boolRead(c1)) {
+            this.value = v1;
+        } else {
+            this.value = null;
+        }
+    }
+
+    private boolean boolRead(boolean b){
+        return b;
+    }
+}

latte/src/test/java/AppTest.java

@@ -40,7 +40,9 @@ private static Stream<Arguments> provideCorrectTestCases() {
             Arguments.of("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java"),
             Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"),
             Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"),
-            Arguments.of("src/test/examples/stack_overflow/MediaRecord.java")
+            Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"),
+            Arguments.of("src/test/examples/MyNodeInvocationIf.java"),
+            Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java")
         );
     }