Skip to content

Commit 3f3fa21

Browse files
authored
If e1 Then s1 'Else skip' adaptation (#21)
## Description Simulated an "Else { skip; }" when no else expression is present in the original code. ## Related Issue Closes #11 ## Type of change - [ ] Bug fix - [x] New feature - [ ] Documentation update - [ ] Code refactoring ## How Has This Been Tested? Some simple feature tests were ran locally, with no found bugs
1 parent f53f95e commit 3f3fa21

6 files changed

Lines changed: 136 additions & 6 deletions

File tree

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

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -534,11 +534,21 @@ public void visitCtIf(CtIf ifElement) {
534534
PermissionEnvironment thenPermEnv = permEnv.cloneLast();
535535
exitScopes();
536536

537-
enterScopes();
538-
super.visitCtBlock(ifElement.getElseStatement());
539-
SymbolicEnvironment elseSymbEnv = symbEnv.cloneLast();
540-
PermissionEnvironment elsePermEnv = permEnv.cloneLast();
541-
exitScopes();
537+
SymbolicEnvironment elseSymbEnv;
538+
PermissionEnvironment elsePermEnv;
539+
540+
if (ifElement.getElseStatement() != null) {
541+
//Else statement
542+
enterScopes();
543+
super.visitCtBlock(ifElement.getElseStatement());
544+
elseSymbEnv = symbEnv.cloneLast();
545+
elsePermEnv = permEnv.cloneLast();
546+
exitScopes();
547+
} else {
548+
//No Else statement
549+
elseSymbEnv = symbEnv.cloneLast();
550+
elsePermEnv = permEnv.cloneLast();
551+
}
542552

543553
joining(thenSymbEnv, thenPermEnv, elseSymbEnv, elsePermEnv);
544554
}
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+
}
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+
}
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+
}
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/java/AppTest.java

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,9 @@ 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"),
4447
Arguments.of("src/test/examples/MyNodeInvocationIf.java"),
4548
Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java")
4649
);
@@ -62,7 +65,8 @@ private static Stream<Arguments> provideIncorrectTestCases() {
6265
Arguments.of("src/test/examples/SmallestIncorrectExample.java", "UNIQUE but got BORROWED"),
6366
Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"),
6467
Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"),
65-
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE")
68+
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"),
69+
Arguments.of("src/test/examples/MyNodeIncorrectIfPermission.java", "Expected UNIQUE but got SHARED")
6670
);
6771
}
6872

0 commit comments

Comments
 (0)