Skip to content

first Contribute #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 10 commits into from
Apr 25, 2025
Merged

first Contribute #13

Changes from 4 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
7fd7efa
resolve conflicts
kiranraoboinapally Apr 21, 2025
9123d31
t rebase --continue
kiranraoboinapally Apr 21, 2025
af30064
Parameterized
kiranraoboinapally Apr 21, 2025
d5d88e9
final
kiranraoboinapally Apr 21, 2025
f3dea87
comment
kiranraoboinapally Apr 21, 2025
f5d139d
comments
kiranraoboinapally Apr 21, 2025
0f1a2e6
comments
kiranraoboinapally Apr 21, 2025
fefed7e
feat(tests): refactor AppTest to separate correct and incorrect test …
kiranraoboinapally Apr 22, 2025
d9e5508
updated pom.xml and AppTest with javadoc
kiranraoboinapally Apr 24, 2025
9ba864c
Throws exception in App and improves error messages in AppTest
CatarinaGamboa Apr 25, 2025
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
318 changes: 62 additions & 256 deletions latte/src/test/java/AppTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,285 +1,91 @@


import static org.junit.Assert.assertTrue;
import static org.junit.jupiter.api.Assertions.assertFalse;
import static org.junit.jupiter.api.Assertions.assertTrue;
import static org.junit.jupiter.api.Assertions.fail;

import java.util.ArrayList;
import java.util.logging.Logger;
import java.util.stream.Stream;

import org.junit.Test;
import org.junit.jupiter.api.Test;
import org.junit.jupiter.params.ParameterizedTest;
import org.junit.jupiter.params.provider.Arguments;
import org.junit.jupiter.params.provider.MethodSource;

import api.App;
import context.SymbolicEnvironment;
import context.SymbolicValue;
import typechecking.LatteException;
import api.App;
/**
* Unit test for simple App.
*/
public class AppTest {

/*
* Correct Examples
*/
@Test
public void testMyNodeCorrect(){
try {
App.launcher("src/test/examples/MyNodeCorrect.java");
} catch (Exception e) {
assert(false);
}
}

@Test
public void testMyNodePush(){
try {
App.launcher("src/test/examples/MyNodePush.java");
} catch (Exception e) {
assert(false);
}
}

@Test
public void testMyNodePushPop(){
try {
App.launcher("src/test/examples/MyNodePushPop.java");
} catch (Exception e) {
assert(false);
}

}

@Test
public void testMyNodeComplete(){
try {
App.launcher("src/test/examples/MyNodeComplete.java");
} catch (Exception e) {
assert(false);
}

}

@Test
public void testMyStackFieldAssign(){
try {
App.launcher("src/test/examples/MyStackFieldAssign.java");
} catch (Exception e) {
assert(false);
}

}

@Test
public void testBox1(){
try {
App.launcher("src/test/examples/BoxMain.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}


@Test
public void testHttpEntityNoAnnotations(){
try {
App.launcher("src/test/examples/HttpEntityNoAnnotations.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testURLConnectionReuseConnection(){
try {
App.launcher("src/test/examples/searching_state_space/URLConnectionReuseConnection.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testURLConnectionSetProperty1(){
try {
App.launcher("src/test/examples/searching_state_space/URLConnectionSetProperty1.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testURLConnectionSetPropertyMultipleShort(){
try {
App.launcher("src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testTimerTaskCannotReschedule(){
try {
App.launcher("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testResultSetNoNext(){
try {
App.launcher("src/test/examples/searching_state_space/ResultSetNoNext.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testResultSetForwardOnly(){
try {
App.launcher("src/test/examples/searching_state_space/ResultSetForwardOnly.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

@Test
public void testSOSMediaRecord(){
try {
App.launcher("src/test/examples/stack_overflow/MediaRecord.java");
} catch (Exception e) {
e.printStackTrace();
assert(false);
}
}

/*
* Incorrect Examples
*/

@Test
public void testMyNode(){
try {
App.launcher("src/test/examples/MyNode.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("UNIQUE but got BORROWED"));
}

}

@Test
public void testMyNodePushPopIncorrect(){
try {
App.launcher("src/test/examples/MyNodePushPopIncorrect.java");
} catch (Exception e) {
System.out.println(e.getMessage());
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("FREE but got BOTTOM"));
}

}

@Test
public void testMyNodeNoDistinct(){
try {
App.launcher("src/test/examples/MyNodeNoDistinct.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("Non-distinct parameters"));
}
}

@Test
public void testMyNodeCallUniqueFree(){
try {
App.launcher("src/test/examples/MyNodeCallUniqueFree.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("FREE but got UNIQUE"));
}

}

@Test
public void testSmallestIncorrectExample(){
try {
App.launcher("src/test/examples/SmallestIncorrectExample.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("UNIQUE but got BORROWED"));
}

}

@Test
public void testMyStackFieldAssignMethod(){
try {
App.launcher("src/test/examples/MyStackFieldAssignMethod.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("UNIQUE but got SHARED"));
}
}

@Test
public void testFieldAccessNoThis(){
try {
App.launcher("src/test/examples/FieldAccessNoThis.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("UNIQUE but got SHARED"));
}
}

@Test
public void testFieldAccessRightNoThis(){
try {
App.launcher("src/test/examples/FieldAccessRightNoThis.java");
} catch (Exception e) {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains("FREE but got UNIQUE"));
}
}

public class AppTest {

@Test
public void testReachabilityUnitTest(){
private static Stream<Arguments> provideTestCases() {
return Stream.of(
Arguments.of("src/test/examples/MyNodeCorrect.java", true, null),
Arguments.of("src/test/examples/MyNodePush.java", true, null),
Arguments.of("src/test/examples/MyNodePushPop.java", true, null),
Arguments.of("src/test/examples/MyNodeComplete.java", true, null),
Arguments.of("src/test/examples/MyStackFieldAssign.java", true, null),
Arguments.of("src/test/examples/BoxMain.java", true, null),
Arguments.of("src/test/examples/HttpEntityNoAnnotations.java", true, null),
Arguments.of("src/test/examples/searching_state_space/URLConnectionReuseConnection.java", true, null),
Arguments.of("src/test/examples/searching_state_space/URLConnectionSetProperty1.java", true, null),
Arguments.of("src/test/examples/searching_state_space/URLConnectionSetPropertyMultipleShort.java", true, null),
Arguments.of("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java", true, null),
Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java", true, null),
Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java", true, null),
Arguments.of("src/test/examples/stack_overflow/MediaRecord.java", true, null),
Arguments.of("src/test/examples/MyNode.java", false, "UNIQUE but got BORROWED"),
Comment thread
kiranraoboinapally marked this conversation as resolved.
Outdated
Arguments.of("src/test/examples/MyNodePushPopIncorrect.java", false, "FREE but got BOTTOM"),
Arguments.of("src/test/examples/MyNodeNoDistinct.java", false, "Non-distinct parameters"),
Arguments.of("src/test/examples/MyNodeCallUniqueFree.java", false, "FREE but got UNIQUE"),
Arguments.of("src/test/examples/SmallestIncorrectExample.java", false, "UNIQUE but got BORROWED"),
Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", false, "UNIQUE but got SHARED"),
Arguments.of("src/test/examples/FieldAccessNoThis.java", false, "UNIQUE but got SHARED"),
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", false, "FREE but got UNIQUE")
);
}

@ParameterizedTest
@MethodSource("provideTestCases")
public void testApp(String filePath, boolean shouldPass, String expectedErrorMessage) {
try {
App.launcher(filePath);
if (!shouldPass) {
fail("Expected an exception but none was thrown.");
}
} catch (Exception e) {
if (shouldPass) {
fail("Unexpected exception: " + e.getMessage());
} else {
assertTrue(e instanceof LatteException);
assertTrue(e.getMessage().contains(expectedErrorMessage));
}
}
}

@Test
public void testReachabilityUnitTest() {
Logger logger = Logger.getLogger(AppTest.class.getName());
//test
SymbolicEnvironment se = new SymbolicEnvironment();
se.enterScope();
SymbolicValue v1 = se.addVariable("x");
// x->1
SymbolicValue v2 = se.addVariable("y");
Comment thread
kiranraoboinapally marked this conversation as resolved.
// x->1; y->2
SymbolicValue v3 = se.addField(v1,"f");
// x->1; y->2, 1.f->3
SymbolicValue v3 = se.addField(v1, "f");
se.addVarSymbolicValue("z", v1);
SymbolicValue v4 = se.get("z");
// x->1; y->2, 1.f->3, z -> 1

logger.info(se.toString());

boolean b = se.canReach(v1, v2, new ArrayList<>());
logger.info(v1.toString() + " can reach " + v2.toString() + "? " + b);
logger.info(v1.toString() + " can reach " + v2.toString() + "? " + b);
assertFalse(b);

boolean b1 = se.canReach(v1, v3, new ArrayList<>());
logger.info(v1.toString() + " can reach " + v3.toString() + "? " + b1);
logger.info(v1.toString() + " can reach " + v3.toString() + "? " + b1);
assertTrue(b1);


boolean b2 = se.canReach(v1, v4, new ArrayList<>());
logger.info(v1.toString() + " can reach " + v4.toString() + "? " + b1);
logger.info(v1.toString() + " can reach " + v4.toString() + "? " + b1);
assertTrue(b2);
}


}
}