diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 63d07c6..3bec793 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/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); } diff --git a/latte/src/test/examples/MyNodeIfInvocationPermission.java b/latte/src/test/examples/MyNodeIfInvocationPermission.java new file mode 100644 index 0000000..73eca3d --- /dev/null +++ b/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; + } +} diff --git a/latte/src/test/examples/MyNodeInvocationIf.java b/latte/src/test/examples/MyNodeInvocationIf.java new file mode 100644 index 0000000..5f44a1e --- /dev/null +++ b/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; + } +} diff --git a/latte/src/test/java/AppTest.java b/latte/src/test/java/AppTest.java index 8bd0f59..5a47da7 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -40,7 +40,9 @@ private static Stream 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") ); }