Skip to content

Commit efa029f

Browse files
PichersPichers
authored
Merge branch 'main' into external-libraries
2 parents 611660a + 3f3fa21 commit efa029f

8 files changed

Lines changed: 219 additions & 6 deletions

File tree

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

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -547,6 +547,8 @@ public void visitCtIf(CtIf ifElement) {
547547
visitCtVariableRead((CtVariableRead<?>)condition);
548548
} else if (condition instanceof CtFieldRead){
549549
visitCtFieldRead((CtFieldRead<?>)condition);
550+
} else if (condition instanceof CtInvocation) {
551+
visitCtInvocation((CtInvocation<?>) condition);
550552
} else {
551553
logError("Cannot evaluate the condition of the if statement: " + condition.toString(), condition);
552554
}
@@ -557,11 +559,21 @@ public void visitCtIf(CtIf ifElement) {
557559
PermissionEnvironment thenPermEnv = permEnv.cloneLast();
558560
exitScopes();
559561

560-
enterScopes();
561-
super.visitCtBlock(ifElement.getElseStatement());
562-
SymbolicEnvironment elseSymbEnv = symbEnv.cloneLast();
563-
PermissionEnvironment elsePermEnv = permEnv.cloneLast();
564-
exitScopes();
562+
SymbolicEnvironment elseSymbEnv;
563+
PermissionEnvironment elsePermEnv;
564+
565+
if (ifElement.getElseStatement() != null) {
566+
//Else statement
567+
enterScopes();
568+
super.visitCtBlock(ifElement.getElseStatement());
569+
elseSymbEnv = symbEnv.cloneLast();
570+
elsePermEnv = permEnv.cloneLast();
571+
exitScopes();
572+
} else {
573+
//No Else statement
574+
elseSymbEnv = symbEnv.cloneLast();
575+
elsePermEnv = permEnv.cloneLast();
576+
}
565577

566578
joining(thenSymbEnv, thenPermEnv, elseSymbEnv, elsePermEnv);
567579
}

‎latte/src/test/examples/MyNodeAllKindsIfs.java‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
6+
/*
7+
* This file is part of the Latte test suite.
8+
*/
9+
class MyNode {
10+
11+
@Unique Object value;
12+
@Unique Node next;
13+
14+
/**
15+
* Constructor for the Node class using @Free value and next nodes
16+
* @param value
17+
* @param next
18+
*/
19+
public MyNode (@Free Object value, @Free Node next) {
20+
this.value = value;
21+
this.next = next;
22+
}
23+
24+
public Object test(@Free Object v1, @Free Object v2, boolean c1, boolean c2){
25+
if (c1) {
26+
this.value = v1;
27+
} else if (c2) {
28+
this.value = v2;
29+
} else {
30+
this.value = v1;
31+
}
32+
33+
if (c2 || this.value == null) {
34+
this.value = v1;
35+
} else {
36+
this.value = v2;
37+
}
38+
if (c1 && this.value == v1) {
39+
this.value = v2;
40+
}
41+
return this.value;
42+
}
43+
}

‎latte/src/test/examples/MyNodeIfInvocationPermission.java‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
import specification.Shared;
6+
7+
/*
8+
* This file is part of the Latte test suite.
9+
*/
10+
class MyNode {
11+
12+
@Unique Object value;
13+
@Unique Node next;
14+
15+
/**
16+
* Constructor for the Node class using @Free value and next nodes
17+
* @param value
18+
* @param next
19+
*/
20+
public MyNode (@Free Object value, @Free Node next) {
21+
this.value = value;
22+
this.next = next;
23+
}
24+
25+
public @Unique Object test(@Free Object v1, @Free Object v2, @Free Node n1, boolean c1){
26+
@Shared MyNode n = new MyNode(v1, n1);
27+
Object o1 = new Object();
28+
Node n2 = new Node();
29+
30+
if (this.test(n, o1, n2)) {
31+
this.value = v2;
32+
} else {
33+
this.value = v2;
34+
}
35+
return this.value;
36+
}
37+
38+
public boolean test2(@Shared MyNode node, @Free Object o, @Free Node next){
39+
@Free MyNode mn = new MyNode(o, next);
40+
node = mn;
41+
42+
return node == this;
43+
}
44+
}

‎latte/src/test/examples/MyNodeIfNoElse.java‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
6+
/*
7+
* This file is part of the Latte test suite.
8+
*/
9+
class MyNode {
10+
11+
@Unique Object value;
12+
@Unique Node next;
13+
14+
/**
15+
* Constructor for the Node class using @Free value and next nodes
16+
* @param value
17+
* @param next
18+
*/
19+
public MyNode (@Free Object value, @Free Node next) {
20+
this.value = value;
21+
this.next = next;
22+
}
23+
24+
public Object test(@Free Object v1, boolean c1){
25+
if (c1) {
26+
this.value = v1;
27+
}
28+
return this.value;
29+
}
30+
}

‎latte/src/test/examples/MyNodeIfPermissionCheck.java‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
6+
class MyNodeIfNoElse {
7+
8+
@Unique Object value;
9+
10+
public @Unique Object test(@Free Object v1, boolean cond) {
11+
Object n;
12+
n = new Object();
13+
14+
this.value = n;
15+
if (cond) {
16+
this.value = v1;
17+
}
18+
return this.value; // should still be @Unique
19+
}
20+
}

‎latte/src/test/examples/MyNodeIncorrectIfPermission.java‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
import specification.Shared;
6+
import specification.Borrowed;
7+
8+
class MyNodeIfNoElse {
9+
10+
@Unique Object value;
11+
12+
public @Unique Object test(@Shared Object v1, boolean cond) {
13+
Object n;
14+
n = new Object();
15+
16+
this.value = n;
17+
if (cond) {
18+
this.value = v1;
19+
}
20+
21+
return this.value;
22+
}
23+
}

‎latte/src/test/examples/MyNodeInvocationIf.java‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
package latte;
2+
3+
import specification.Free;
4+
import specification.Unique;
5+
6+
/*
7+
* This file is part of the Latte test suite.
8+
*/
9+
class MyNode {
10+
11+
@Unique Object value;
12+
@Unique Node next;
13+
14+
/**
15+
* Constructor for the Node class using @Free value and next nodes
16+
* @param value
17+
* @param next
18+
*/
19+
public MyNode (@Free Object value, @Free Node next) {
20+
this.value = value;
21+
this.next = next;
22+
}
23+
24+
public void test(@Free Object v1, boolean c1){
25+
if (boolRead(c1)) {
26+
this.value = v1;
27+
} else {
28+
this.value = null;
29+
}
30+
}
31+
32+
private boolean boolRead(boolean b){
33+
return b;
34+
}
35+
}

‎latte/src/test/java/AppTest.java‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,11 @@ private static Stream<Arguments> provideCorrectTestCases() {
4141
Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"),
4242
Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"),
4343
Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"),
44+
Arguments.of("src/test/examples/MyNodeAllKindsIfs.java"),
45+
Arguments.of("src/test/examples/MyNodeIfNoElse.java"),
46+
Arguments.of("src/test/examples/MyNodeIfPermissionCheck.java"),
47+
Arguments.of("src/test/examples/MyNodeInvocationIf.java"),
48+
Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java"),
4449
Arguments.of("src/test/examples/LinkedListRefinement.java")
4550
);
4651
}
@@ -62,7 +67,8 @@ private static Stream<Arguments> provideIncorrectTestCases() {
6267
Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"),
6368
Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"),
6469
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"),
65-
Arguments.of("src/test/examples/LinkedListRefinementIncorrect.java", "FREE but got UNIQUE")
70+
Arguments.of("src/test/examples/MyNodeIncorrectIfPermission.java", "Expected UNIQUE but got SHARED"),
71+
Arguments.of("src/test/examples/LinkedListRefinementIncorrect.java", "FREE but got UNIQUE")
6672
);
6773
}
6874

0 commit comments

Comments
 (0)