Multiple Errors

liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java

@@ -4,102 +4,16 @@
 
 class SimpleTest {
 
-    @Refinement("return > 0")
-    public int test() {
-        return 10;
+    void test1() {
+        @Refinement("x > 0")
+        int x = -1;
     }
-}
-
-// @RefinementAlias("Percentage(int x) { 0 <= x && x <= 100 }")
-// @Refinement("Percentage(_)")
-// public static int addBonus(
-//                  @Refinement("Percentage(grade)") int grade,
-//                  @Refinement("Percentage(bonus) && (bonus < grade)")
-//                  int bonus) {
-//
-//    if((grade + bonus) > 100)
-//        return 100;
-//
-//    else
-//        return grade+bonus;
-// }
-//
-
-//		@Refinement("_ > 10")
-//		int i = 10;
-
-//		@Refinement("sum(_) > 30")
-//		Account a = new Account(50);
-//		a.deposit(60);
-
-//		Account b = new Account(138);
-//		b = a.transferTo(b, 10);
-//
-//		@Refinement("sum(_) == 148")
-//		Account c = b;
-
-//		Order o = new Order();
-//
-//		Order f = o.addItem("shirt", 60).addGift();
-//				.getNewOrderPayThis().addItem("t", 6).addItem("t", 1);
-//		o.addGift();
-//		f.addItem("l", 1).pay(000).addGift().pay(000);//.addTransportCosts().sendToAddress("home");
-
-//		TrafficLight tl = new TrafficLight();
-//		tl.transitionToAmber();
-//
-
-//		TrafficLight tl2 = tl.getTrafficLightStartingRed();
-//		tl2.transitionToFlashingAmber();
-
-//		tl.transitionToAmber();
-//		tl.transitionToAmber();
-
-//		tl.passagersCross();
-//		tl.intermitentMalfunction();
 
-//		tl.transitionToFlashingAmber();
+    void test2() {
+        @Refinement("y > 0")
+        int y = -2;
 
-//		@Refinement("size(al) < 4")
-//		ArrayList<Integer> al = new ArrayList<Integer>();
-//		al.add(1);
-//		al.add(1);
-//		al.get(2);
-
-//		@Refinement("size(t) == 3")
-//		ArrayList<Integer> t = al;
-
-//
-//		Order o = new Order();
-//		o.addItem("shirt", 5)
-//		 .addItem("shirt", 10)
-//		 .addItem("h", 20)
-//		 .addItem("h", 6);
-
-//	InputStreamReader isr = new InputStreamReader(System.in);
-//	isr.read();
-//	isr.read();
-//	isr.read();
-//	isr.close();
-//
-//	//...
-//	isr.read();
-
-//	@Refinement("_ > 0")
-//	public int fun (int[] arr) {
-//		return max(arr[0], 1);
-//	}
-//
-
-//		//@Refinement("_.length(x) >= 0") ==
-////	@Refinement("length(_, x) >= 0")
-////	int[] a1 = new int[5];
-// K(.., ..)
-
-//	}
-
-// See error NaN
-//		@Refinement("true")
-//		double b = 0/0;
-//		@Refinement("_ > 5")
-//		double c = b;
+        @Refinement("z > 0")
+        int z = 3;
+    }
+}

liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java

@@ -0,0 +1,19 @@
+package testMultiple;
+
+import liquidjava.specification.Refinement;
+
+class MultipleErrorsExample {
+
+    void test1() {
+        @Refinement("a > 0")
+        int a = -1;
+    }
+
+    void test2() {
+        @Refinement("b > 0")
+        int b = -2;
+
+        @Refinement("c > 0")
+        int c = -3;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java → liquidjava-example/src/main/java/testMultiple/errors/CustomError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.StateSet;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java → liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.Ghost;
 import liquidjava.specification.StateRefinement;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java → liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.StateRefinement;
 import liquidjava.specification.StateSet;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java → liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.Refinement;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java → liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.Refinement;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java → liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.Refinement;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java → liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.StateRefinement;
 import liquidjava.specification.StateSet;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java → liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.StateRefinement;
 import liquidjava.specification.StateSet;

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java → liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.errors;
+package testMultiple.errors;
 
 import liquidjava.specification.Refinement;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java → liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.warnings;
+package testMultiple.warnings;
 
 import liquidjava.specification.ExternalRefinementsFor;
 

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java → liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.warnings;
+package testMultiple.warnings;
 
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.RefinementPredicate;

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java → liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java

@@ -1,4 +1,4 @@
-package testingInProgress.diagnostics.warnings;
+package testMultiple.warnings;
 
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.RefinementPredicate;

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.1</version>
+	<version>0.0.2</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -1,11 +1,10 @@
 package liquidjava.api;
 
-import static liquidjava.diagnostics.Diagnostics.diagnostics;
-
 import java.io.File;
 import java.util.Arrays;
 import java.util.List;
 
+import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.CustomError;
 import liquidjava.processor.RefinementProcessor;
 import spoon.Launcher;
@@ -15,6 +14,9 @@
 import spoon.support.QueueProcessingManager;
 
 public class CommandLineLauncher {
+
+    private static final Diagnostics diagnostics = Diagnostics.getInstance();
+
     public static void main(String[] args) {
         if (args.length == 0) {
             System.out.println("No input paths provided");
@@ -26,17 +28,20 @@ public static void main(String[] args) {
         }
         List<String> paths = Arrays.asList(args);
         launch(paths.toArray(new String[0]));
+
+        // print diagnostics
+        System.out.println(diagnostics.getWarningOutput());
         if (diagnostics.foundError()) {
             System.out.println(diagnostics.getErrorOutput());
         } else {
-            System.out.println(diagnostics.getWarningOutput());
             System.out.println("Correct! Passed Verification.");
         }
     }
 
     public static void launch(String... paths) {
         System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", ""));
 
+        diagnostics.clear();
         Launcher launcher = new Launcher();
         for (String path : paths) {
             if (!new File(path).exists()) {
@@ -49,7 +54,6 @@ public static void launch(String... paths) {
         launcher.getEnvironment().setNoClasspath(true);
         launcher.getEnvironment().setComplianceLevel(8);
         launcher.run();
-        diagnostics.clear();
 
         final Factory factory = launcher.getFactory();
         final ProcessingManager processingManager = new QueueProcessingManager(factory);

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java

@@ -1,6 +1,6 @@
 package liquidjava.diagnostics;
 
-import java.util.ArrayList;
+import java.util.LinkedHashSet;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.warnings.LJWarning;
 
@@ -11,24 +11,26 @@
  * @see LJWarning
  */
 public class Diagnostics {
-    public static final Diagnostics diagnostics = new Diagnostics();
+    private static final Diagnostics instance = new Diagnostics();
 
-    private ArrayList<LJError> errors;
-    private ArrayList<LJWarning> warnings;
+    private LinkedHashSet<LJError> errors;
+    private LinkedHashSet<LJWarning> warnings;
 
     private Diagnostics() {
-        this.errors = new ArrayList<>();
-        this.warnings = new ArrayList<>();
+        this.errors = new LinkedHashSet<>();
+        this.warnings = new LinkedHashSet<>();
+    }
+
+    public static Diagnostics getInstance() {
+        return instance;
     }
 
     public void add(LJError error) {
-        if (!this.errors.contains(error))
-            this.errors.add(error);
+        this.errors.add(error);
     }
 
     public void add(LJWarning warning) {
-        if (!this.warnings.contains(warning))
-            this.warnings.add(warning);
+        this.warnings.add(warning);
     }
 
     public boolean foundError() {
@@ -39,52 +41,25 @@ public boolean foundWarning() {
         return !this.warnings.isEmpty();
     }
 
-    public ArrayList<LJError> getErrors() {
+    public LinkedHashSet<LJError> getErrors() {
         return this.errors;
     }
 
-    public ArrayList<LJWarning> getWarnings() {
+    public LinkedHashSet<LJWarning> getWarnings() {
         return this.warnings;
     }
 
-    public LJError getError() {
-        return foundError() ? this.errors.get(0) : null;
-    }
-
-    public LJWarning getWarning() {
-        return foundWarning() ? this.warnings.get(0) : null;
-    }
-
     public void clear() {
         this.errors.clear();
         this.warnings.clear();
     }
 
     public String getErrorOutput() {
-        StringBuilder sb = new StringBuilder();
-        if (foundError()) {
-            for (LJError error : errors) {
-                sb.append(error.toString()).append("\n");
-            }
-        } else {
-            if (foundWarning()) {
-                sb.append("Warnings:\n");
-                for (LJWarning warning : warnings) {
-                    sb.append(warning.getMessage()).append("\n");
-                }
-                sb.append("Passed Verification!\n");
-            }
-        }
-        return sb.toString();
+        return String.join("\n", errors.stream().map(LJError::toString).toList()) + (errors.isEmpty() ? "" : "\n");
     }
 
     public String getWarningOutput() {
-        StringBuilder sb = new StringBuilder();
-        if (foundWarning()) {
-            for (LJWarning warning : warnings) {
-                sb.append(warning.toString()).append("\n");
-            }
-        }
-        return sb.toString();
+        return String.join("\n", warnings.stream().map(LJWarning::toString).toList())
+                + (warnings.isEmpty() ? "" : "\n");
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -6,7 +6,7 @@
 
 import spoon.reflect.cu.SourcePosition;
 
-public class LJDiagnostic {
+public class LJDiagnostic extends RuntimeException {
 
     private String title;
     private String message;
@@ -49,8 +49,8 @@ public String toString() {
         StringBuilder sb = new StringBuilder();
 
         // title
-        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
-                .append("\n");
+        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET)
+                .append(message.toLowerCase()).append("\n");
 
         // snippet
         String snippet = getSnippet();
@@ -113,7 +113,6 @@ public String getSnippet() {
             }
             return sb.toString();
         } catch (Exception e) {
-            e.printStackTrace();
             return null;
         }
     }