Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions latte/src/main/java/typechecking/LatteTypeChecker.java
Original file line number Diff line number Diff line change
Expand Up @@ -522,6 +522,12 @@ public void visitCtIf(CtIf ifElement) {
visitCtVariableRead((CtVariableRead<?>)condition);
} else if (condition instanceof CtFieldRead){
visitCtFieldRead((CtFieldRead<?>)condition);
} else if (condition instanceof CtInvocation) {
CtInvocation<?> invocation = (CtInvocation<?>) condition;
if (!invocation.getType().getQualifiedName().equals("boolean")) {
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need to check this as the Java compiler already performs this check

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);
}
Expand Down
35 changes: 35 additions & 0 deletions latte/src/test/examples/MyNodeInvocationIf.java
Original file line number Diff line number Diff line change
@@ -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)) {
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now add more tests with methods that use the Objects with permissions like @Unique, and see if their changes are added to the context after the call.

this.value = v1;
} else {
this.value = null;
}
}

private boolean boolRead(boolean b){
return b;
}
}
3 changes: 2 additions & 1 deletion latte/src/test/java/AppTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,8 @@ 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")
);
}

Expand Down
Loading