From 7cd03884977e3711fbece00f50bb7c55e4b4d8ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 17:10:00 +0100 Subject: [PATCH 1/5] Added support for function invocation in If condition --- latte/src/main/java/typechecking/LatteTypeChecker.java | 2 ++ 1 file changed, 2 insertions(+) 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); } From 49a2af0f5ff78240227a9d643cdce9e3db77faed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 17:54:16 +0100 Subject: [PATCH 2/5] Added a check for invication return type (must be boolean) --- latte/src/main/java/typechecking/LatteTypeChecker.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 3bec793..3320eb8 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -523,7 +523,11 @@ public void visitCtIf(CtIf ifElement) { } else if (condition instanceof CtFieldRead){ visitCtFieldRead((CtFieldRead)condition); } else if (condition instanceof CtInvocation) { - visitCtInvocation((CtInvocation) condition); + CtInvocation invocation = (CtInvocation) condition; + if (!invocation.getType().getQualifiedName().equals("boolean")) { + logError("Method invoked in if condition must return boolean", condition); + } + visitCtInvocation(invocation); } else { logError("Cannot evaluate the condition of the if statement: " + condition.toString(), condition); } From 088781b9857441c51f8ef7f1cfca5352b4042b20 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 18:05:40 +0100 Subject: [PATCH 3/5] Added related test # Conflicts: # latte/src/test/java/AppTest.java --- .../src/test/examples/MyNodeInvocationIf.java | 35 +++++++++++++++++++ latte/src/test/java/AppTest.java | 3 +- 2 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 latte/src/test/examples/MyNodeInvocationIf.java 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..d679fbc 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -40,7 +40,8 @@ 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") ); } From eeeac5d0b15339350d1a32a3de329f70696ece9c Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Sun, 15 Jun 2025 17:25:15 +0100 Subject: [PATCH 4/5] removed java type check --- latte/src/main/java/typechecking/LatteTypeChecker.java | 6 +----- latte/src/test/examples/MyNodeIfInvocationPermission.java | 0 2 files changed, 1 insertion(+), 5 deletions(-) create mode 100644 latte/src/test/examples/MyNodeIfInvocationPermission.java diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 3320eb8..3bec793 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -523,11 +523,7 @@ public void visitCtIf(CtIf ifElement) { } else if (condition instanceof CtFieldRead){ visitCtFieldRead((CtFieldRead)condition); } else if (condition instanceof CtInvocation) { - CtInvocation invocation = (CtInvocation) condition; - if (!invocation.getType().getQualifiedName().equals("boolean")) { - logError("Method invoked in if condition must return boolean", condition); - } - visitCtInvocation(invocation); + 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..e69de29 From 43d69459f1472358f03c69462d35e0e6a76b603b Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Sun, 15 Jun 2025 17:42:51 +0100 Subject: [PATCH 5/5] Added new test for permission check after invocations in if condition --- .../MyNodeIfInvocationPermission.java | 44 +++++++++++++++++++ latte/src/test/java/AppTest.java | 3 +- 2 files changed, 46 insertions(+), 1 deletion(-) diff --git a/latte/src/test/examples/MyNodeIfInvocationPermission.java b/latte/src/test/examples/MyNodeIfInvocationPermission.java index e69de29..73eca3d 100644 --- a/latte/src/test/examples/MyNodeIfInvocationPermission.java +++ 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/java/AppTest.java b/latte/src/test/java/AppTest.java index d679fbc..5a47da7 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -41,7 +41,8 @@ private static Stream provideCorrectTestCases() { 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/MyNodeInvocationIf.java") + Arguments.of("src/test/examples/MyNodeInvocationIf.java"), + Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java") ); }