Skip to content

Commit da236d1

Browse files
fix test file and test cases
1 parent 3dce154 commit da236d1

File tree

6 files changed

+44
-43
lines changed

6 files changed

+44
-43
lines changed

liquidjava-example/src/main/java/testSuite/field_updates/IncorrectFieldUpdate.java renamed to liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@
22

33
import liquidjava.specification.StateRefinement;
44

5-
public class IncorrectFieldUpdate {
5+
public class ErrorFieldUpdate {
66
public int n;
77

88
@StateRefinement(from = "n(this) > 0", to = "n(this) == n(old(this))")
99
public void shouldFailIfFieldIsNegative() {}
1010

1111
public static void main(String[] args) {
1212

13-
IncorrectFieldUpdate t = new IncorrectFieldUpdate();
13+
ErrorFieldUpdate t = new ErrorFieldUpdate();
1414
t.n = -1;
1515
t.shouldFailIfFieldIsNegative();
1616
}

liquidjava-example/src/main/java/testSuite/math/correctInvocation/CorrectInvocationFromMathLibrary.java renamed to liquidjava-example/src/main/java/testSuite/math/correctInvocation/InvocationFromMathLibrary.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import liquidjava.specification.Refinement;
44

55
@SuppressWarnings("unused")
6-
public class CorrectInvocationFromMathLibrary {
6+
public class InvocationFromMathLibrary {
77
public static void main(String[] args) {
88

99
// Math.abs(...)

liquidjava-example/src/main/java/testSuite/math/errorAbs/ErrorMathAbs.java renamed to liquidjava-example/src/main/java/testSuite/math/errorAbs/MathAbs.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import liquidjava.specification.Refinement;
44

55
@SuppressWarnings("unused")
6-
public class ErrorMathAbs {
6+
public class MathAbs {
77
public static void main(String[] args) {
88
@Refinement("true")
99
int ab = Math.abs(-9);

liquidjava-example/src/main/java/testSuite/math/errorMax/ErrorMathAbs.java renamed to liquidjava-example/src/main/java/testSuite/math/errorMax/MathAbs.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import liquidjava.specification.Refinement;
44

55
@SuppressWarnings("unused")
6-
public class ErrorMathAbs {
6+
public class MathAbs {
77
public static void main(String[] args) {
88
@Refinement("true")
99
int ab = Math.abs(-9);

liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/ErrorMathMultiplyExact.java renamed to liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/MathMultiplyExact.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
import liquidjava.specification.Refinement;
44

55
@SuppressWarnings("unused")
6-
public class ErrorMathMultiplyExact {
6+
public class MathMultiplyExact {
77
public static void main(String[] args) {
88
@Refinement("_ == 40")
99
int mul = Math.multiplyExact(5, 8);

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java

Lines changed: 38 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -16,57 +16,58 @@
1616

1717
public class TestExamples {
1818

19+
/**
20+
* Test the file at the given path by launching the verifier and checking for errors. The file/directory is expected
21+
* to be either correct or contain an error based on its name.
22+
*
23+
* @param filePath
24+
* path to the file to test
25+
*/
1926
@ParameterizedTest
2027
@MethodSource("fileNameSource")
2128
public void testFile(final Path filePath) {
2229
String fileName = filePath.getFileName().toString();
23-
System.out.println("Testing file: " + fileName);
30+
31+
// 1. Run the verifier on the file or package
32+
ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString());
2433

25-
// For Regular Files in the root directory check their name
26-
if (Files.isRegularFile(filePath)) {
27-
ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString());
28-
System.out.println(
29-
errorEmitter.foundError() ? (errorEmitter.getFullMessage()) : ("Correct! Passed Verification."));
30-
31-
if (fileName.startsWith("Correct") && errorEmitter.foundError()) {
32-
System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found");
33-
fail();
34-
}
35-
if (fileName.startsWith("Error") && !errorEmitter.foundError()) {
36-
System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification");
37-
fail();
38-
}
39-
} else // For Directories and subdirectories check if they contain "error" or "correct" in their name
40-
if (Files.isDirectory(filePath) && (fileName.contains("error") || fileName.contains("correct"))) {
41-
ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString());
42-
System.out.println(
43-
errorEmitter.foundError() ? (errorEmitter.getFullMessage()) : ("Correct! Passed Verification."));
44-
45-
if (fileName.contains("correct") && errorEmitter.foundError()) {
46-
System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found");
47-
fail();
48-
}
49-
if (fileName.contains("error") && !errorEmitter.foundError()) {
50-
System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification");
51-
fail();
52-
}
34+
// 2. Check if the file is correct or contains an error
35+
if ((fileName.startsWith("Correct") && errorEmitter.foundError())
36+
|| (fileName.contains("correct") && errorEmitter.foundError())) {
37+
System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found");
38+
fail();
39+
}
40+
// 3. Check if the file has an error but passed verification
41+
if ((fileName.startsWith("Error") && !errorEmitter.foundError())
42+
|| (fileName.contains("error") && !errorEmitter.foundError())) {
43+
System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification");
44+
fail();
5345
}
5446
}
5547

48+
/**
49+
* Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with
50+
* "Correct" or "Error", and directories containing "correct" or "error".
51+
*
52+
* @return Stream of paths to test files
53+
*
54+
* @throws IOException
55+
* if an I/O error occurs or the path does not exist
56+
*/
5657
private static Stream<Path> fileNameSource() throws IOException {
5758
return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE,
5859
(filePath, fileAttr) -> {
59-
// Get the parent directory path (root directory)
60-
Path rootDir = Paths.get("../liquidjava-example/src/main/java/testSuite/");
61-
62-
// 1. Files only in the root directory
63-
boolean isFileInRootDir = fileAttr.isRegularFile() && filePath.getParent().equals(rootDir);
60+
String name = filePath.getFileName().toString();
61+
// 1. Files that start with "Correct" or "Error"
62+
boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile()
63+
&& (name.startsWith("Correct") || name.startsWith("Error"));
6464

65-
// 2. Directories and subdirectories (recursive search for directories)
66-
boolean isDirectory = fileAttr.isDirectory();
65+
// 2. Folders (directories) that contain "correct" or "error"
66+
boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory()
67+
&& (name.contains("correct") || name.contains("error"));
6768

6869
// Return true if either condition matches
69-
return isFileInRootDir || isDirectory;
70+
return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError;
7071
});
7172
}
7273
}

0 commit comments

Comments
 (0)