diff --git a/.gitattributes b/.gitattributes
new file mode 100644
index 00000000..94f480de
--- /dev/null
+++ b/.gitattributes
@@ -0,0 +1 @@
+* text=auto eol=lf
\ No newline at end of file
diff --git a/README.md b/README.md
index 1e20ac80..39352ea3 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,7 @@
# LiquidJava - Extending Java with Liquid Types
+[](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java)
+[](https://central.sonatype.com/artifact/io.github.liquid-java/liquidjava-api)
+
@@ -49,7 +52,7 @@ Additionally, you'll need the following dependency, which includes the LiquidJav
io.github.liquid-java
liquidjava-api
- 0.0.3
+ 0.0.4
```
@@ -60,7 +63,7 @@ repositories {
}
dependencies {
- implementation 'io.github.liquid-java:liquidjava-api:0.0.3'
+ implementation 'io.github.liquid-java:liquidjava-api:0.0.4'
}
```
@@ -78,8 +81,6 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project
```bash
mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project"
```
-*Warning: Any change to LiquidJava requires rebuilding the jar.*
-
If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process.
@@ -105,10 +106,14 @@ The starter test file is `TestExamples.java`, which runs the test suite under th
The test suite considers test cases:
1. Files that start with `Correct` or `Error` (e.g., `CorrectRecursion.java`)
-2. Packages or folders that contain the word `correct` or `error` (e.g., `arraylist_correct`)
+2. Directories that contain the word `correct` or `error` (e.g., `arraylist_correct`)
Therefore, the files and folders that do not follow this pattern are ignored.
+For failing test cases, the expected error must be specified as follows:
+1. In singular test files, the expected error (title) should be written in the first line of the file as a comment
+2. In test directories, a `.expected` file should be included in that directory with the expected error (title)
+
## Project Structure
* **docs**: Contains documents used for the design of the language. This folder includes a [README](./docs/design/README.md) with the link to the full artifact used in the design process. It also contains initial documents used to prepare the design of the refinements language during its evaluation
diff --git a/liquidjava-api/pom.xml b/liquidjava-api/pom.xml
index 88bbe565..ca68b54b 100644
--- a/liquidjava-api/pom.xml
+++ b/liquidjava-api/pom.xml
@@ -11,7 +11,7 @@
io.github.liquid-java
liquidjava-api
- 0.0.3
+ 0.0.4
liquidjava-api
LiquidJava API
https://github.com/liquid-java/liquidjava
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java b/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java
index 1ed03d84..3faef58e 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/ExternalRefinementsFor.java
@@ -6,18 +6,37 @@
import java.lang.annotation.Target;
/**
- * Annotation to create refinements for an external library. The annotation receives the path of the
- * library e.g. @ExternalRefinementsFor("java.lang.Math")
+ * Annotation to refine a class or interface of an external library.
+ *
+ * This annotation allows you to specify refinements and state transitions for classes from external libraries
+ * that you cannot directly annotate. The refinements apply to all instances of the specified class.
+ *
+ * Example:
+ *
+ * {@code
+ * @ExternalRefinementsFor("java.lang.Math")
+ * public interface MathRefinements {
+ * @Refinement("_ >= 0")
+ * public double sqrt(double x);
+ * }
+ * }
+ *
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
public @interface ExternalRefinementsFor {
+
/**
- * The prefix of the external method
- *
- * @return
+ * The fully qualified name of the class or interface for which the refinements are being defined.
+ *
+ * Example:
+ *
+ * {@code
+ * @ExternalRefinementsFor("java.lang.Math")
+ * }
+ *
*/
- public String value();
+ String value();
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java
index 7fb600e4..195b5693 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/Ghost.java
@@ -7,15 +7,37 @@
import java.lang.annotation.Target;
/**
- * Annotation to create a ghost variable for a class. The annotation receives
- * the type and name of
- * the ghost within a string e.g. @Ghost("int size")
+ * Annotation to create a ghost variable for a class or interface.
+ *
+ * Ghost variables that only exist during the verification and can be used in refinements and state refinements.
+ * They are not part of the actual implementation but help specify behavior and invariants.
+ *
+ * Example:
+ *
+ * {@code
+ * @Ghost("int size")
+ * public class MyStack {
+ * // ...
+ * }
+ * }
+ *
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
@Repeatable(GhostMultiple.class)
public @interface Ghost {
- public String value();
+
+ /**
+ * The type and name of the ghost variable.
+ *
+ * Example:
+ *
+ * {@code
+ * @Ghost("int size")
+ * }
+ *
+ */
+ String value();
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java
index 8b42d74a..4aea5a73 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/GhostMultiple.java
@@ -6,9 +6,9 @@
import java.lang.annotation.Target;
/**
- * Annotation to allow the creation of multiple @Ghost
+ * Annotation to allow the creation of multiple ghost variables.
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
index ce3dc20a..0048435b 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
@@ -6,14 +6,49 @@
import java.lang.annotation.Target;
/**
- * Annotation to add a refinement to variables, class fields, method's parameters and method's
- * return value e.g. @Refinement("x > 0") int x;
+ * Annotation to add a refinement to variables, class fields, method's parameters and method's return values.
+ *
+ * Refinements are logical predicates that must hold for the annotated element.
+ *
+ * Example:
+ *
+ * {@code
+ * @Refinement("x > 0")
+ * int x;
+ *
+ * @Refinement("_ > 0")
+ * int increment(@Refinement("_ >= 0") int n) {
+ * return n + 1;
+ * }
+ *
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.FIELD, ElementType.LOCAL_VARIABLE, ElementType.PARAMETER, ElementType.TYPE})
public @interface Refinement {
- public String value();
+ /**
+ * The refinement string that defines a logical predicate that must hold for the annotated element.
+ *
+ * Example:
+ *
+ * {@code
+ * @Refinement("x > 0")
+ * }
+ *
+ */
+ String value();
+
+ /**
+ * Custom error message to be shown when the refinement is violated (optional).
+ *
+ * Example:
+ *
+ * {@code
+ * @Refinement(value = "x > 0", msg = "x must be positive")
+ * }
+ *
+ */
+ String msg() default "";
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java
index 5274514a..01253d56 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAlias.java
@@ -7,14 +7,39 @@
import java.lang.annotation.Target;
/**
- * Annotation to create a ghost variable for a class. The annotation receives the type and name of
- * the ghost within a string e.g. @RefinementAlias("Nat(int x) {x > 0}")
+ * Annotation to create a refinement alias to be reused in refinements.
+ *
+ * Refinement aliases can be used to define reusable refinement predicates with parameters.
+ * They help reduce duplication and improve readability of complex refinement specifications.
+ *
+ * Example:
+ *
+ * {@code
+ * @RefinementAlias("Nat(int x) { x > 0 }")
+ * public class MyClass {
+ * @Refinement("Nat(_)")
+ * int value;
+ * }
+ * }
+ *
*
- * @author catarina gamboa
+ * @see Refinement
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
@Repeatable(RefinementAliasMultiple.class)
public @interface RefinementAlias {
- public String value();
+
+ /**
+ * The refinement alias string, which includes the name of the alias, its parameters and the refinement itself.
+ *
+ * Example:
+ *
+ * {@code
+ * @RefinementAlias("Nat(int x) { x > 0 }")
+ * }
+ *
+ */
+ String value();
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java
index a4b2256e..2f5e93e0 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementAliasMultiple.java
@@ -6,9 +6,9 @@
import java.lang.annotation.Target;
/**
- * Annotation to create a multiple Alias in a class
+ * Annotation to create multiple refinement aliases.
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
index aabea663..44d7f4df 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicate.java
@@ -6,9 +6,41 @@
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
+/**
+ * Annotation that allows the creation of ghost variables or refinement aliases within method or constructor scope.
+ *
+ * This annotation enables the declaration of ghosts and refinement aliases.
+ *
+ * Example:
+ *
+ * {@code
+ * @RefinementPredicate("ghost int size")
+ * @RefinementPredicate("type Nat(int x) { x > 0 }")
+ * public void process() {
+ * // ...
+ * }
+ * }
+ *
+ *
+ * @see Ghost
+ * @see RefinementAlias
+ * @author Catarina Gamboa
+ */
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@Repeatable(RefinementPredicateMultiple.class)
public @interface RefinementPredicate {
- public String value();
+
+ /**
+ * The refinement predicate string, which can define a ghost variable or a refinement alias.
+ *
+ * Example:
+ *
+ * {@code
+ * @RefinementPredicate("ghost int size")
+ * @RefinementPredicate("type Nat(int x) { x > 0 }")
+ * }
+ *
+ */
+ String value();
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
index 3af7267b..ca512fa8 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/RefinementPredicateMultiple.java
@@ -5,6 +5,11 @@
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
+/**
+ * Annotation to allow the creation of multiple refinement predicates.
+ *
+ * @author Catarina Gamboa
+ */
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
public @interface RefinementPredicateMultiple {
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
index b652944b..2d235891 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
@@ -7,18 +7,63 @@
import java.lang.annotation.Target;
/**
- * Annotation to create state transitions in a method. The annotation has two arguments: from : the
- * state in which the object needs to be for the method to be invoked correctly to : the state in
- * which the object will be after the execution of the method
- * e.g. @StateRefinement(from="open(this)", to="closed(this)")
+ * Annotation to create state transitions in a method using states defined in state sets.
+ *
+ * This annotation specifies the required precondition state and the resulting
+ * postcondition state when a method or constructor is invoked.
+ * Constructors can only specify the postcondition state since they create a new object.
+ *
+ * Example:
+ *
+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+ * public void close() {
+ * // ...
+ * }
+ * }
+ *
*
- * @author catarina gamboa
+ * @see StateSet
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@Repeatable(StateRefinementMultiple.class)
public @interface StateRefinement {
- public String from() default "";
- public String to() default "";
+ /**
+ * The logical pre-condition that defines the state in which the object needs to be before calling the method (optional)
+ *
+ * Example:
+ *
+ * {@code
+ * @StateRefinement(from="open(this)")
+ * }
+ *
+ */
+ String from() default "";
+
+ /**
+ * The logical post-condition that defines the state in which the object will be after calling the method (optional)
+ *
+ * Example:
+ *
+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)")
+ * }
+ *
+ */
+ String to() default "";
+
+ /**
+ * Custom error message to be shown when the {@code from} pre-condition is violated (optional)
+ *
+ * Example:
+ *
+ * {@code
+ * @StateRefinement(from="open(this)", to="closed(this)", msg="The object needs to be open before closing")
+ * }
+ *
+ */
+ String msg() default "";
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java
index 0280fcbe..c410a4db 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/StateRefinementMultiple.java
@@ -6,10 +6,9 @@
import java.lang.annotation.Target;
/**
- * Interface to allow multiple state refinements in a method. A method can have a state refinement
- * for each set of different source and destination states
+ * Annotation to allow the creation of multiple state transitions.
*
- * @author catarina gamboa
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
index 71549eca..ccdc4ebb 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java
@@ -7,15 +7,39 @@
import java.lang.annotation.Target;
/**
- * Annotation to create the disjoint states in which class objects can be. The annotation receives a
- * list of strings representing the names of the states. e.g. @StateSet({"open", "reading",
- * "closed"})
+ * Annotation to create a set of disjoint states in which class objects can be.
+ *
+ * An object will always be in exactly one state from each state set at any given time,
+ * and cannot be in more than one state from the same state set (e.g., {@code open} and {@code closed} simultaneously).
+ * To allow an object to be in multiple states at once, they must be from different state sets.
+ *
+ * Example:
+ *
+ * {@code
+ * @StateSet({"open", "reading", "closed"})
+ * @StateSet({"locked", "unlocked"})
+ * public class File {
+ * // ...
+ * }
+ *
*
- * @author catarina gamboa
+ * @see StateRefinement
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
@Repeatable(StateSets.class)
public @interface StateSet {
- public String[] value();
+
+ /**
+ * The array of states to be created.
+ *
+ * Example:
+ *
+ * {@code
+ * @StateSet({"open", "reading", "closed"})
+ * }
+ *
+ */
+ String[] value();
}
diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
index ecd10fdf..817a0c91 100644
--- a/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
+++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSets.java
@@ -6,9 +6,8 @@
import java.lang.annotation.Target;
/**
- * Interface to allow multiple StateSets in a class.
- *
- * @author catarina gamboa
+ * Annotation to allow the creation of multiple state sets.
+ * @author Catarina Gamboa
*/
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE})
diff --git a/liquidjava-example/pom.xml b/liquidjava-example/pom.xml
index ef167bc6..2ad19908 100644
--- a/liquidjava-example/pom.xml
+++ b/liquidjava-example/pom.xml
@@ -50,7 +50,7 @@
io.github.liquid-java
liquidjava-api
- 0.0.3
+ 0.0.4
diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java
index 48999074..1d2feab6 100644
--- a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java
+++ b/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 al = new ArrayList();
-// al.add(1);
-// al.add(1);
-// al.get(2);
-
-// @Refinement("size(t) == 3")
-// ArrayList 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;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java b/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java
new file mode 100644
index 00000000..a46cde56
--- /dev/null
+++ b/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;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/CustomError.java b/liquidjava-example/src/main/java/testMultiple/errors/CustomError.java
new file mode 100644
index 00000000..7505005d
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/CustomError.java
@@ -0,0 +1,8 @@
+package testMultiple.errors;
+
+import liquidjava.specification.StateSet;
+
+@StateSet({"Open", "Closed"})
+public class CustomError {
+
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java b/liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java
new file mode 100644
index 00000000..831c6ca5
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java
@@ -0,0 +1,11 @@
+package testMultiple.errors;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+public class GhostInvocationError {
+
+ @StateRefinement(to="size(this, this) == 0")
+ public void test() {}
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java b/liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java
new file mode 100644
index 00000000..01134b29
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java
@@ -0,0 +1,11 @@
+package testMultiple.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class IllegalConstructorTransitionError {
+
+ @StateRefinement(from="open(this)", to="closed(this)")
+ public IllegalConstructorTransitionError() {}
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java
new file mode 100644
index 00000000..e81cfdff
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java
@@ -0,0 +1,10 @@
+package testMultiple.errors;
+
+import liquidjava.specification.Refinement;
+
+public class InvalidRefinementError {
+ public static void main(String[] args) {
+ @Refinement("_ + 1")
+ int x = 5;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java b/liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java
new file mode 100644
index 00000000..df3b7d93
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java
@@ -0,0 +1,11 @@
+package testMultiple.errors;
+
+import liquidjava.specification.Refinement;
+
+public class NotFoundError {
+
+ public static void main(String[] args) {
+ @Refinement("x > 0")
+ int y = 1;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java
new file mode 100644
index 00000000..b6ab1682
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java
@@ -0,0 +1,11 @@
+package testMultiple.errors;
+
+import liquidjava.specification.Refinement;
+
+public class RefinementError {
+
+ public static void main(String[] args) {
+ @Refinement("x > 0")
+ int x = -1;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java b/liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java
new file mode 100644
index 00000000..66b8b9ae
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java
@@ -0,0 +1,14 @@
+package testMultiple.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateConflictError {
+
+ @StateRefinement(to="open(this)")
+ public StateConflictError() {}
+
+ @StateRefinement(from="open(this) && closed(this)")
+ public void close() {}
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java
new file mode 100644
index 00000000..1187de24
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java
@@ -0,0 +1,20 @@
+package testMultiple.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateRefinementError {
+
+ @StateRefinement(to="open(this)")
+ public StateRefinementError() {}
+
+ @StateRefinement(from="!closed(this)", to="closed(this)")
+ public void close() {}
+
+ public static void main(String[] args) {
+ StateRefinementError s = new StateRefinementError();
+ s.close();
+ s.close();
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java b/liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java
new file mode 100644
index 00000000..082d25b8
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java
@@ -0,0 +1,11 @@
+package testMultiple.errors;
+
+import liquidjava.specification.Refinement;
+
+public class SyntaxError {
+
+ public static void main(String[] args) {
+ @Refinement("x $ 0")
+ int x = -1;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java
new file mode 100644
index 00000000..c1506822
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java
@@ -0,0 +1,8 @@
+package testMultiple.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+
+@ExternalRefinementsFor("non.existent.Class")
+public interface NonExistentClass {
+ public void NonExistentClass();
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java
new file mode 100644
index 00000000..eae37e3c
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java
@@ -0,0 +1,16 @@
+package testMultiple.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface NonExistentConstructor {
+
+ @RefinementPredicate("int size(ArrayList l)")
+ @StateRefinement(to = "size(this) == 0")
+ public void ArrayList(String wrongParameter);
+
+ @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+ public boolean add(E e);
+}
diff --git a/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java
new file mode 100644
index 00000000..9d3d16e6
--- /dev/null
+++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java
@@ -0,0 +1,16 @@
+package testMultiple.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface NonExistentMethod {
+
+ @RefinementPredicate("int size(ArrayList l)")
+ @StateRefinement(to = "size(this) == 0")
+ public void ArrayList();
+
+ @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+ public boolean add(String e);
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java
new file mode 100644
index 00000000..1a404775
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectBoxedTypes.java
@@ -0,0 +1,18 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectBoxedTypes {
+ public static void main(String[] args) {
+ @Refinement("_ == true")
+ Boolean b = true;
+
+ @Refinement("_ > 0")
+ Integer i = 1;
+
+ @Refinement("_ > 0")
+ Double d = 1.0;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java
new file mode 100644
index 00000000..8eb1174c
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationIncrementOnce.java
@@ -0,0 +1,21 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int n")
+public class CorrectDotNotationIncrementOnce {
+
+ // explicit this
+ @StateRefinement(to="this.n() == 0")
+ public CorrectDotNotationIncrementOnce() {}
+
+ // implicit this
+ @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
+ public void incrementOnce() {}
+
+ public static void main(String[] args) {
+ CorrectDotNotationIncrementOnce t = new CorrectDotNotationIncrementOnce();
+ t.incrementOnce();
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java
new file mode 100644
index 00000000..aaef95fe
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectDotNotationTrafficLight.java
@@ -0,0 +1,27 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"green", "amber", "red"})
+public class CorrectDotNotationTrafficLight {
+
+ @StateRefinement(to="this.green()")
+ public CorrectDotNotationTrafficLight() {}
+
+ @StateRefinement(from="this.green()", to="this.amber()")
+ public void transitionToAmber() {}
+
+ @StateRefinement(from="red()", to="green()")
+ public void transitionToGreen() {}
+
+ @StateRefinement(from="this.amber()", to="red()")
+ public void transitionToRed() {}
+
+ public static void main(String[] args) {
+ CorrectDotNotationTrafficLight tl = new CorrectDotNotationTrafficLight();
+ tl.transitionToAmber();
+ tl.transitionToRed();
+ tl.transitionToGreen();
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java
index 30ac3840..b8ceddb7 100644
--- a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java
+++ b/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java
@@ -36,4 +36,31 @@ public static void main(String[] args) {
@Refinement("_ > 10")
long f = doubleBiggerThanTwenty(2 * 80);
}
+
+
+ void testSmallLong() {
+ @Refinement("v > 0")
+ long v = 42L;
+ }
+
+ void testDoublePrecisionBoundary() {
+ @Refinement("v == 9007199254740993")
+ long v = 9007199254740993L;
+ }
+
+ void testLargeSubtraction() {
+ @Refinement("v - 9007199254740992 == 1")
+ long v = 9007199254740993L;
+ }
+
+ void testMaxValueModulo() {
+ @Refinement("v % 1000 == 807")
+ long v = 9223372036854775807L;
+ }
+
+ void testUUID(){
+ @Refinement("((v/4096) % 16) == 1")
+ long v = 0x01000000122341666L;
+ }
+
}
diff --git a/liquidjava-example/src/main/java/testSuite/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/CorrectSimple.java
similarity index 87%
rename from liquidjava-example/src/main/java/testSuite/SimpleTest.java
rename to liquidjava-example/src/main/java/testSuite/CorrectSimple.java
index 8821c0c9..c9096799 100644
--- a/liquidjava-example/src/main/java/testSuite/SimpleTest.java
+++ b/liquidjava-example/src/main/java/testSuite/CorrectSimple.java
@@ -3,7 +3,7 @@
import liquidjava.specification.Refinement;
@SuppressWarnings("unused")
-public class SimpleTest {
+public class CorrectSimple {
public static void main(String[] args) {
// Arithmetic Binary Operations
@Refinement("a >= 10")
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java
index 130434f9..fd375b09 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java
index b6a0816f..3ae6ed8e 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAfterIf2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java
index 4cc2b496..7ed25815 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAlias.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAlias.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java
index 6e3682cd..a5dd6c75 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java
@@ -1,3 +1,4 @@
+// Argument Mismatch Error
package testSuite;
import liquidjava.specification.Refinement;
@@ -8,7 +9,7 @@
public class ErrorAliasArgumentSize {
public static void main(String[] args) {
- @Refinement("InRange( _, 10)")
+ @Refinement("InRange(j, 10)")
int j = 15;
}
}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java
new file mode 100644
index 00000000..99231431
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java
@@ -0,0 +1,15 @@
+// Argument Mismatch Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+
+@SuppressWarnings("unused")
+@RefinementAlias("InRange(int val, int low, int up) {low < val && val < up}")
+public class ErrorAliasEmptyArguments {
+
+ public static void main(String[] args) {
+ @Refinement("InRange()")
+ int j = 15;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java
new file mode 100644
index 00000000..ca21871a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java
@@ -0,0 +1,12 @@
+// Not Found Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorAliasNotFound {
+
+ public static void main(String[] args) {
+ @Refinement("UndefinedAlias(x)")
+ int x = 5;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
index ce751d5c..1e2f1787 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasSimple.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
index 074765a0..263a0f9b 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java
@@ -1,3 +1,4 @@
+// Argument Mismatch Error
package testSuite;
import liquidjava.specification.Refinement;
@@ -14,6 +15,5 @@ public static void main(String[] args) {
@Refinement("Positive(_)")
double positive = positiveGrade2;
- // Positive(_) fica positive > 0
}
}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java
index 9556fea0..b2add7fa 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticBinaryOperations.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java
index b5798484..45239bc6 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP1.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java
index ab60cb9b..16e58df7 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java
index 0e96412d..ae85bc50 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP3.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java
index 51706603..88eed94c 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorArithmeticFP4.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java
index 83b31147..60acfbd7 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorAssignementAfterDeclaration.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java
index 029fd4dc..99cc67d6 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanFunInvocation.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java
index 0ad3ded1..09b97f7e 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorBooleanLiteral.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java
new file mode 100644
index 00000000..93c6a3c1
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedBoolean {
+ public static void main(String[] args) {
+ @Refinement("_ == true")
+ Boolean b = false;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java
new file mode 100644
index 00000000..643b509a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedDouble {
+ public static void main(String[] args) {
+ @Refinement("_ > 0")
+ Double d = -1.0;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java
new file mode 100644
index 00000000..2d937e20
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java
@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorBoxedInteger {
+ public static void main(String[] args) {
+ @Refinement("_ > 0")
+ Integer j = -1;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java
index d8d5715d..9c83af5e 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorDependentRefinement.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java
new file mode 100644
index 00000000..8bf06584
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationIncrementOnce.java
@@ -0,0 +1,21 @@
+// State Refinement Error
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int n")
+public class ErrorDotNotationIncrementOnce {
+
+ @StateRefinement(to="this.n() == 0")
+ public ErrorDotNotationIncrementOnce() {}
+
+ @StateRefinement(from="n() == 0", to="n() == old(this).n() + 1")
+ public void incrementOnce() {}
+
+ public static void main(String[] args) {
+ ErrorDotNotationIncrementOnce t = new ErrorDotNotationIncrementOnce();
+ t.incrementOnce();
+ t.incrementOnce(); // error
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java
new file mode 100644
index 00000000..483309b3
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationMultiple.java
@@ -0,0 +1,18 @@
+// Syntax Error
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+public class ErrorDotNotationMultiple {
+
+ @StateRefinement(to="size() == 0")
+ public ErrorDotNotationMultiple() {}
+
+ void test() {
+ @Refinement("_ == this.not.size()")
+ int x = 0;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java
new file mode 100644
index 00000000..e40ddb30
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorDotNotationTrafficLight.java
@@ -0,0 +1,28 @@
+// State Refinement Error
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"green", "amber", "red"})
+public class ErrorDotNotationTrafficLight {
+
+ @StateRefinement(to="this.green()")
+ public ErrorDotNotationTrafficLight() {}
+
+ @StateRefinement(from="this.green()", to="this.amber()")
+ public void transitionToAmber() {}
+
+ @StateRefinement(from="red()", to="green()")
+ public void transitionToGreen() {}
+
+ @StateRefinement(from="this.amber()", to="red()")
+ public void transitionToRed() {}
+
+ public static void main(String[] args) {
+ ErrorDotNotationTrafficLight tl = new ErrorDotNotationTrafficLight();
+ tl.transitionToAmber();
+ tl.transitionToGreen(); // error
+ tl.transitionToRed();
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java
index 99f6f435..e2184b67 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionDeclarations.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java
index a8439044..f1ca6bf7 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java
index 26119616..e4309a4c 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocation1.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java
index ba398c67..6d1fa473 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorFunctionInvocationParams.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
index 5fce2f7d..6ff3be00 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java
@@ -1,3 +1,4 @@
+// Argument Mismatch Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java
new file mode 100644
index 00000000..be2af75c
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java
@@ -0,0 +1,12 @@
+// Not Found Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorGhostNotFound {
+
+ public void test() {
+ @Refinement("notFound(x)")
+ int x = 5;
+ }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java
index f080428c..f9b8ef35 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java
@@ -1,3 +1,4 @@
+// Argument Mismatch Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java
index 90c225c5..06c61126 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java
index c66c4b71..19692a5a 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorIfAssignment2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java
index e34f2c4d..41061023 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorImplementationSearchValueIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java
index 04e2f523..2aadc688 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLenZeroIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java
index aef298bb..2bc1d1f6 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage1.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java
index 61a482d3..fe5a231a 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsage2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java
new file mode 100644
index 00000000..55504b0d
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java
@@ -0,0 +1,11 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorLongUsagePredicates1 {
+ void testUUID(){
+ @Refinement("((v/4096) % 16) == 2")
+ long v = 0x01000000122341666L;
+ }
+}
\ No newline at end of file
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java
new file mode 100644
index 00000000..fc760314
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java
@@ -0,0 +1,11 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorLongUsagePredicates2 {
+ void testLargeSubtractionWrong() {
+ @Refinement("v - 9007199254740992 == 2")
+ long v = 9007199254740993L;
+ }
+}
\ No newline at end of file
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java
new file mode 100644
index 00000000..e5412994
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java
@@ -0,0 +1,11 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorLongUsagePredicates3 {
+ void testWrongSign() {
+ @Refinement("v < 0")
+ long v = 42L;
+ }
+}
\ No newline at end of file
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java
index 52c2c758..f53bf558 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorMissingAliasTypeParameter.java
@@ -1,3 +1,4 @@
+// Syntax Error
package testSuite;
import liquidjava.specification.RefinementAlias;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java
index 2db74f88..c2133b27 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorNoRefinementsInVar.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java
index 7b5b9fe6..518d351e 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorRecursion1.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java
index e25c2c13..54ac3507 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchIntArray.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java
index ad63b279..f7a96890 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray1.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java
index d9f482ea..944b7e6f 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSearchValueIntArray2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java
index a00d4069..d07f1259 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java
index 1a63afc4..65bdde9b 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificArithmetic.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java
index b15b633e..04704a8e 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java
index c1e373c3..2cae544c 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificValuesIf2.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java
index 6ec09838..ccb34136 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java
index 7e1d1c22..c00f5b90 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java
similarity index 79%
rename from liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java
rename to liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java
index bdf498ae..b02c63d0 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorSyntax1.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxRefinement.java
@@ -1,9 +1,10 @@
+// Syntax Error
package testSuite;
import liquidjava.specification.Refinement;
@SuppressWarnings("unused")
-public class ErrorSyntax1 {
+public class ErrorSyntaxRefinement {
public static void main(String[] args) {
@Refinement("_ < 100 +")
int value = 90 + 4;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java
new file mode 100644
index 00000000..14fd6a2b
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorSyntaxStateRefinement.java
@@ -0,0 +1,10 @@
+// Syntax Error
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+
+public class ErrorSyntaxStateRefinement {
+
+ @StateRefinement(from="$", to="#")
+ void test() {}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java
index 4543463b..2c89393a 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorTernaryExpression.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java
index 018db95a..3b50f615 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorTrafficLightRGB.java
@@ -1,3 +1,4 @@
+// State Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java
index 6583832f..2981a217 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorTypeInRefinements.java
@@ -1,3 +1,4 @@
+// Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java
index 85149333..73eb1529 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOpMinus.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java
index dbc59590..b8660ea8 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java
+++ b/liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java
@@ -1,3 +1,4 @@
+// Refinement Error
package testSuite;
import liquidjava.specification.Refinement;
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java
similarity index 76%
rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java
rename to liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java
index 800ee7c0..b79eaa87 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java
+++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java
@@ -3,6 +3,6 @@
import liquidjava.specification.ExternalRefinementsFor;
@ExternalRefinementsFor("non.existent.Class")
-public interface ErrorExtRefNonExistentClass {
+public interface WarningExtRefNonExistentClass {
public void NonExistentClass();
}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java
similarity index 89%
rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java
rename to liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java
index 78b1c8c9..b98e48db 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java
+++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java
@@ -5,7 +5,7 @@
import liquidjava.specification.StateRefinement;
@ExternalRefinementsFor("java.util.ArrayList")
-public interface ErrorExtRefNonExistentMethod {
+public interface WarningExtRefNonExistentMethod {
@RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java
similarity index 90%
rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java
rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java
index 636d3adb..a81ee0ed 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java
+++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java
@@ -5,7 +5,7 @@
import liquidjava.specification.StateRefinement;
@ExternalRefinementsFor("java.util.ArrayList")
-public interface ErrorExtRefWrongConstructor {
+public interface WarningExtRefWrongConstructor {
@RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java
similarity index 89%
rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java
rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java
index da2135c5..c847d9e7 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java
+++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java
@@ -5,7 +5,7 @@
import liquidjava.specification.StateRefinement;
@ExternalRefinementsFor("java.util.ArrayList")
-public interface ErrorExtRefWrongParameterType {
+public interface WarningExtRefWrongParameterType {
@RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java
similarity index 90%
rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java
rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java
index 48509080..bbba0b9a 100644
--- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java
+++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java
@@ -5,7 +5,7 @@
import liquidjava.specification.StateRefinement;
@ExternalRefinementsFor("java.util.ArrayList")
-public interface ErrorExtRefWrongRetType {
+public interface WarningExtRefWrongRetType {
@RefinementPredicate("int size(ArrayList l)")
@StateRefinement(to = "size(this) == 0")
diff --git a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java
index 6580fab7..80e2741c 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/ErrorGhostState.java
@@ -1,3 +1,4 @@
+// Error
package testSuite.classes;
import liquidjava.specification.Ghost;
diff --git a/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/boolean_ghost_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/email_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/index_out_of_bounds_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/input_reader_error2/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/method_overload_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/order_gift_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_interface_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/refs_from_superclass_error/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/scoreboard_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected
new file mode 100644
index 00000000..49d2a05a
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/socket_error/.expected
@@ -0,0 +1 @@
+State Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected
new file mode 100644
index 00000000..258d98bb
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/classes/state_multiple_error/.expected
@@ -0,0 +1 @@
+State Conflict Error
diff --git a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java
index 4aeaf01e..55a10184 100644
--- a/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java
+++ b/liquidjava-example/src/main/java/testSuite/field_updates/ErrorFieldUpdate.java
@@ -1,3 +1,4 @@
+// State Refinement Error
package testSuite.field_updates;
import liquidjava.specification.StateRefinement;
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/math/errorAbs/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/math/errorMax/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected
new file mode 100644
index 00000000..6f476981
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/math/errorMultiplyExact/.expected
@@ -0,0 +1 @@
+Refinement Error
diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml
index e9727bff..65b45140 100644
--- a/liquidjava-verifier/pom.xml
+++ b/liquidjava-verifier/pom.xml
@@ -11,7 +11,7 @@
io.github.liquid-java
liquidjava-verifier
- 0.0.1
+ 0.0.12
liquidjava-verifier
LiquidJava Verifier
https://github.com/liquid-java/liquidjava
@@ -301,7 +301,7 @@
io.github.liquid-java
liquidjava-api
- 0.0.3
+ 0.0.4
diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
index e34f40ad..d6f7f45f 100644
--- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
+++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
@@ -37,13 +37,17 @@ literalExpression:
'(' literalExpression ')' #litGroup
| literal #lit
| ID #var
- | ID '.' functionCall #targetInvocation
| functionCall #invocation
;
functionCall:
ghostCall
- | aliasCall;
+ | aliasCall
+ | dotCall;
+
+dotCall:
+ OBJECT_TYPE '(' args? ')'
+ | ID '(' args? ')' '.' ID '(' args? ')';
ghostCall:
ID '(' args? ')';
diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java
index dc6aa2b4..b664ced6 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java
@@ -4,73 +4,74 @@
import java.util.Arrays;
import java.util.List;
-import liquidjava.diagnostics.ErrorEmitter;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.CustomError;
+import liquidjava.diagnostics.warnings.CustomWarning;
import liquidjava.processor.RefinementProcessor;
import spoon.Launcher;
+import spoon.compiler.Environment;
import spoon.processing.ProcessingManager;
import spoon.reflect.declaration.CtPackage;
import spoon.reflect.factory.Factory;
import spoon.support.QueueProcessingManager;
public class CommandLineLauncher {
- public static void main(String[] args) {
- // String allPath = "C://Regen/test-projects/src/Main.java";
- // In eclipse only needed this:"../liquidjava-example/src/main/java/"
- // In VSCode needs:
- // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project";
+ private static final Diagnostics diagnostics = Diagnostics.getInstance();
+
+ public static void main(String[] args) {
if (args.length == 0) {
- System.out.println("No input files or directories provided");
+ System.out.println("No input paths provided");
System.out.println("\nUsage: ./liquidjava <...paths>");
- System.out.println(" <...paths>: Paths to files or directories to be verified by LiquidJava");
+ System.out.println(" <...paths>: Paths to be verified by LiquidJava");
System.out.println(
- "\nExample: ./liquidjava liquidjava-example/src/main/java/test/currentlyTesting liquidjava-example/src/main/java/testingInProgress/Account.java");
+ "\nExample: ./liquidjava liquidjava-example/src/main/java/test liquidjava-example/src/main/java/testingInProgress/Account.java");
return;
}
List paths = Arrays.asList(args);
- ErrorEmitter ee = launch(paths.toArray(new String[0]));
- System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification."));
+ launch(paths.toArray(new String[0]));
+
+ // print diagnostics
+ if (diagnostics.foundWarning()) {
+ System.out.println(diagnostics.getWarningOutput());
+ }
+ if (diagnostics.foundError()) {
+ System.out.println(diagnostics.getErrorOutput());
+ } else {
+ System.out.println("Correct! Passed Verification.");
+ }
}
- public static ErrorEmitter launch(String... paths) {
+ public static void launch(String... paths) {
System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", ""));
- ErrorEmitter ee = new ErrorEmitter();
+ diagnostics.clear();
Launcher launcher = new Launcher();
for (String path : paths) {
if (!new File(path).exists()) {
- ee.addError("Path not found", "The path " + path + " does not exist", 1);
- return ee;
+ diagnostics.add(new CustomError("The path " + path + " was not found"));
+ return;
}
launcher.addInputResource(path);
}
- launcher.getEnvironment().setNoClasspath(true);
- // Get the current classpath from the system
- // String classpath = System.getProperty("java.class.path");
- // launcher.getEnvironment().setSourceClasspath(classpath.split(File.pathSeparator));
+ Environment env = launcher.getEnvironment();
+ env.setNoClasspath(true);
+ env.setComplianceLevel(8);
- // optional
- // launcher.getEnvironment().setSourceClasspath(
- // "lib1.jar:lib2.jar".split(":"));
- launcher.getEnvironment().setComplianceLevel(8);
- launcher.run();
+ boolean buildSuccess = launcher.getModelBuilder().build();
+ if (!buildSuccess && (env.getErrorCount() > 0 || env.getWarningCount() > 0)) {
+ diagnostics.add(new CustomWarning("Java compilation encountered issues. Verification may be affected."));
+ }
final Factory factory = launcher.getFactory();
final ProcessingManager processingManager = new QueueProcessingManager(factory);
- final RefinementProcessor processor = new RefinementProcessor(factory, ee);
+ final RefinementProcessor processor = new RefinementProcessor(factory);
processingManager.addProcessor(processor);
- try {
- // analyze all packages
- CtPackage root = factory.Package().getRootPackage();
- if (root != null)
- processingManager.process(root);
- } catch (Exception e) {
- e.printStackTrace();
- throw e;
- }
-
- return ee;
+ // analyze all packages
+ CtPackage root = factory.Package().getRootPackage();
+ if (root != null)
+ processingManager.process(root);
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java
new file mode 100644
index 00000000..7b72d190
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java
@@ -0,0 +1,9 @@
+package liquidjava.diagnostics;
+
+// ANSI color codes
+public class Colors {
+ public static final String RESET = "\u001B[0m";
+ public static final String GREY = "\u001B[90m";
+ public static final String BOLD_RED = "\u001B[1;31m";
+ public static final String BOLD_YELLOW = "\u001B[1;33m";
+}
\ No newline at end of file
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java
new file mode 100644
index 00000000..f125f5fc
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java
@@ -0,0 +1,64 @@
+package liquidjava.diagnostics;
+
+import java.util.LinkedHashSet;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.warnings.LJWarning;
+
+/**
+ * Singleton class to store diagnostics (errors and warnings) during the verification process
+ *
+ * @see LJError
+ * @see LJWarning
+ */
+public class Diagnostics {
+ private static final Diagnostics instance = new Diagnostics();
+
+ private final LinkedHashSet errors;
+ private final LinkedHashSet warnings;
+
+ private Diagnostics() {
+ this.errors = new LinkedHashSet<>();
+ this.warnings = new LinkedHashSet<>();
+ }
+
+ public static Diagnostics getInstance() {
+ return instance;
+ }
+
+ public void add(LJError error) {
+ this.errors.add(error);
+ }
+
+ public void add(LJWarning warning) {
+ this.warnings.add(warning);
+ }
+
+ public boolean foundError() {
+ return !this.errors.isEmpty();
+ }
+
+ public boolean foundWarning() {
+ return !this.warnings.isEmpty();
+ }
+
+ public LinkedHashSet getErrors() {
+ return this.errors;
+ }
+
+ public LinkedHashSet getWarnings() {
+ return this.warnings;
+ }
+
+ public void clear() {
+ this.errors.clear();
+ this.warnings.clear();
+ }
+
+ public String getErrorOutput() {
+ return String.join("\n", errors.stream().map(LJError::toString).toList());
+ }
+
+ public String getWarningOutput() {
+ return String.join("\n", warnings.stream().map(LJWarning::toString).toList());
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java
deleted file mode 100644
index 02610343..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java
+++ /dev/null
@@ -1,92 +0,0 @@
-package liquidjava.diagnostics;
-
-import java.net.URI;
-import java.util.HashMap;
-import liquidjava.processor.context.PlacementInCode;
-import spoon.reflect.cu.SourcePosition;
-
-public class ErrorEmitter {
-
- private String titleMessage;
- private String fullMessage;
- private URI filePath;
- private ErrorPosition position;
- private int errorStatus;
- private HashMap map;
-
- public ErrorEmitter() {
- }
-
- public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus,
- HashMap map) {
- this.titleMessage = titleMessage;
- fullMessage = msg;
- try {
- position = new ErrorPosition(p.getLine(), p.getColumn(), p.getEndLine(), p.getEndColumn());
- filePath = p.getFile().toURI();
- } catch (Exception ignored) {
- fullMessage = "Seems like this error is created in generated part of source code, so no precise"
- + " position is provided. " + fullMessage;
- position = null;
- filePath = null;
- }
- this.errorStatus = errorStatus;
- this.map = map;
- }
-
- public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus) {
- this.titleMessage = titleMessage;
- fullMessage = msg;
- try {
- position = new ErrorPosition(p.getLine(), p.getColumn(), p.getEndLine(), p.getEndColumn());
- filePath = p.getFile().toURI();
- } catch (Exception ignored) {
- fullMessage = "Seems like this error is created in generated part of source code, so no precise"
- + " position is provided. " + fullMessage;
- position = null;
- filePath = null;
- }
- this.errorStatus = errorStatus;
- }
-
- public void addError(String titleMessage, String msg, int errorStatus) {
- this.titleMessage = titleMessage;
- fullMessage = msg;
- this.errorStatus = errorStatus;
- }
-
- public boolean foundError() {
- return fullMessage != null;
- }
-
- public String getTitleMessage() {
- return titleMessage;
- }
-
- public String getFullMessage() {
- return fullMessage;
- }
-
- public URI getFilePath() {
- return filePath;
- }
-
- public void reset() {
- fullMessage = null;
- position = null;
- errorStatus = 0;
- map = null;
- }
-
- public ErrorPosition getPosition() {
- return position;
- }
-
- public int getErrorStatus() {
- return errorStatus;
- }
-
- public HashMap getVCMap() {
- return map;
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java
deleted file mode 100644
index 39452f90..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java
+++ /dev/null
@@ -1,234 +0,0 @@
-package liquidjava.diagnostics;
-
-import java.util.Formatter;
-import java.util.HashMap;
-import java.util.Locale;
-
-import liquidjava.processor.VCImplication;
-import liquidjava.processor.context.PlacementInCode;
-import liquidjava.rj_language.Predicate;
-import spoon.reflect.code.CtLiteral;
-import spoon.reflect.declaration.CtElement;
-
-public class ErrorHandler {
-
- public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
- HashMap map, ErrorEmitter ee) {
- String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
- // cSMT.toString();
-
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- // title
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Failed to check refinement at: \n\n");
- if (moreInfo != null)
- sbtitle.append(moreInfo + "\n");
- sbtitle.append(var.toString());
- // all message
- sb.append(sbtitle.toString() + "\n\n");
- sb.append("Type expected:" + expectedType.toString() + "\n");
- sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n");
- sb.append(printMap(map));
- sb.append("Location: " + var.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
- }
-
- public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
- String states, HashMap map, ErrorEmitter ee) {
-
- String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
- // Found
- // state:"+constraintForErrorMsg.toString()
- // ;
-
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
-
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Failed to check state transitions when calling " + method + " in:\n\n");
- sbtitle.append(element + "\n\n");
-
- sb.append(sbtitle.toString());
- sb.append("Expected possible states:" + states + "\n");
- sb.append("\nState found:\n");
- sb.append(printLine());
- sb.append("\n" + constraintForErrorMsg /* .toConjunctions() */.toString() + "\n");
- sb.append(printLine());
- sb.append("\n");
- sb.append(printMap(map));
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
- }
-
- public static void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
- HashMap map, ErrorEmitter ee) {
-
- String resumeMessage = "Encountered unknown variable";
-
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Encountered unknown variable\n\n");
- sbtitle.append(var + "\n\n");
-
- sb.append(sbtitle.toString());
- sb.append(printMap(map));
- sb.append("Location: " + var.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
- }
-
- public static void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
- HashMap map, ErrorEmitter ee) {
-
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- sb.append(msg);
- sb.append(constraint + "\n");
- sb.append(constraint2 + "\n\n");
- sb.append("Error found while checking conditions in:\n");
- sb.append(var + "\n\n");
- sb.append(printMap(map));
- sb.append("Location: " + var.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(msg, sb.toString(), var.getPosition(), 2, map);
- }
-
- public static void printErrorArgs(CtElement var, Predicate expectedType, String msg,
- HashMap map, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- String title = "Error in ghost invocation: " + msg + "\n";
- sb.append(title);
- sb.append(var + "\nError in refinement:" + expectedType.toString() + "\n");
- sb.append(printMap(map));
- sb.append("Location: " + var.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(title, sb.toString(), var.getPosition(), 2, map);
- }
-
- public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
- HashMap map, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- sb.append(message + "\n\n");
- sb.append(element + "\n");
- sb.append(printMap(map));
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(message, sb.toString(), element.getPosition(), 2, map);
- }
-
- public static void printSameStateSetError(CtElement element, Predicate p, String name,
- HashMap map, ErrorEmitter ee) {
- String resume = "Error found multiple disjoint states from a State Set in a refinement";
-
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Error found multiple disjoint states from a State Set in a refinement\n\n");
- sbtitle.append(element + "\n\n");
- sb.append(sbtitle.toString());
- sb.append("In predicate:" + p.toString() + "\n");
- sb.append("In class:" + name + "\n");
- sb.append(printMap(map));
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(resume, sb.toString(), element.getPosition(), 1, map);
- }
-
- public static void printErrorConstructorFromState(CtElement element, CtLiteral from, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n";
- sb.append(s);
- sb.append(element + "\n\n");
- sb.append("State found:" + from + "\n");
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(s, sb.toString(), element.getPosition(), 1);
- }
-
- public static void printCustomError(CtElement element, String msg, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- String s = "Found Error: " + msg;
- sb.append(s + "\n\n");
- sb.append(element + "\n\n");
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(s, sb.toString(), element.getPosition(), 1);
- }
-
- public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Syntax error with message\n");
- sbtitle.append(msg + "\n");
- sb.append(sbtitle.toString());
- sb.append("Found in refinement:\n");
- sb.append(ref + "\n");
- sb.append("In:\n");
- sb.append(element + "\n");
- sb.append("Location: " + element.getPosition() + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2);
- }
-
- public static void printSyntaxError(String msg, String ref, ErrorEmitter ee) {
- StringBuilder sb = new StringBuilder();
- sb.append("______________________________________________________\n");
- StringBuilder sbtitle = new StringBuilder();
- sbtitle.append("Syntax error with message\n");
- sbtitle.append(msg + "\n");
- sb.append(sbtitle.toString());
- sb.append("Found in refinement:\n");
- sb.append(ref + "\n");
- sb.append("______________________________________________________\n");
-
- ee.addError(sbtitle.toString(), sb.toString(), 2);
- }
-
- private static String printLine() {
- StringBuilder sb = new StringBuilder();
- for (int i = 0; i < 130; i++)
- sb.append("-"); // -----------
- return sb.toString();
- }
-
- private static String printMap(HashMap map) {
- StringBuilder sb = new StringBuilder();
- Formatter formatter = new Formatter(sb, Locale.US);
- if (map.isEmpty()) {
- formatter.close();
- return "";
- }
- formatter.format("\nInstance translation table:\n");
- formatter.format(printLine());
- // title
- formatter.format("\n| %-32s | %-60s | %-1s \n", "Variable Name", "Created in", "File");
- formatter.format(printLine() + "\n");
- // data
- for (String s : map.keySet())
- formatter.format("| %-32s | %-60s | %-1s \n", s, map.get(s).getText(), map.get(s).getSimplePosition());
- // end
- formatter.format(printLine() + "\n\n");
- String s = formatter.toString();
- formatter.close();
- return s;
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java
index 1ee72e7d..3383f6bf 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java
@@ -2,35 +2,7 @@
import spoon.reflect.cu.SourcePosition;
-public class ErrorPosition {
-
- private int lineStart;
- private int colStart;
- private int lineEnd;
- private int colEnd;
-
- public ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) {
- this.lineStart = lineStart;
- this.colStart = colStart;
- this.lineEnd = lineEnd;
- this.colEnd = colEnd;
- }
-
- public int getLineStart() {
- return lineStart;
- }
-
- public int getColStart() {
- return colStart;
- }
-
- public int getLineEnd() {
- return lineEnd;
- }
-
- public int getColEnd() {
- return colEnd;
- }
+public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) {
public static ErrorPosition fromSpoonPosition(SourcePosition pos) {
if (pos == null || !pos.isValidPosition())
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
new file mode 100644
index 00000000..de74d252
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
@@ -0,0 +1,164 @@
+package liquidjava.diagnostics;
+
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+
+import spoon.reflect.cu.SourcePosition;
+
+public class LJDiagnostic extends RuntimeException {
+
+ private final String title;
+ private final String message;
+ private final String accentColor;
+ private final String customMessage;
+ private String file;
+ private ErrorPosition position;
+ private static final String PIPE = " | ";
+
+ public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
+ this.title = title;
+ this.message = message;
+ this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
+ this.position = ErrorPosition.fromSpoonPosition(pos);
+ this.accentColor = accentColor;
+ this.customMessage = customMessage;
+ }
+
+ public String getTitle() {
+ return title;
+ }
+
+ public String getMessage() {
+ return message;
+ }
+
+ public String getCustomMessage() {
+ return customMessage;
+ }
+
+ public String getDetails() {
+ return ""; // to be overridden by subclasses
+ }
+
+ public ErrorPosition getPosition() {
+ return position;
+ }
+
+ public void setPosition(SourcePosition pos) {
+ if (pos == null)
+ return;
+ this.position = ErrorPosition.fromSpoonPosition(pos);
+ this.file = pos.getFile().getPath();
+ }
+
+ public String getFile() {
+ return file;
+ }
+
+ public String getAccentColor() {
+ return accentColor;
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder sb = new StringBuilder();
+
+ // title
+ sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
+ .append("\n");
+
+ // snippet
+ String snippet = getSnippet();
+ if (snippet != null) {
+ sb.append(snippet);
+ }
+
+ // details
+ String details = getDetails();
+ if (!details.isEmpty()) {
+ sb.append(" --> ").append(String.join("\n ", details.split("\n"))).append("\n");
+ }
+
+ // location
+ if (file != null && position != null) {
+ sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n");
+ }
+
+ return sb.toString();
+ }
+
+ public String getSnippet() {
+ if (file == null || position == null)
+ return null;
+
+ Path path = Path.of(file);
+ try {
+ List lines = Files.readAllLines(path);
+ StringBuilder sb = new StringBuilder();
+
+ // before and after lines for context
+ int contextBefore = 2;
+ int contextAfter = 2;
+ int startLine = Math.max(1, position.lineStart() - contextBefore);
+ int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter);
+
+ // calculate padding for line numbers
+ int padding = String.valueOf(endLine).length();
+
+ for (int i = startLine; i <= endLine; i++) {
+ String lineNumStr = String.format("%" + padding + "d", i);
+ String line = lines.get(i - 1);
+
+ // add line
+ sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
+
+ // add error markers on the line(s) with the error
+ if (i >= position.lineStart() && i <= position.lineEnd()) {
+ int colStart = (i == position.lineStart()) ? position.colStart() : 1;
+ int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length();
+
+ if (colStart > 0 && colEnd > 0) {
+ // line number padding + pipe + column offset
+ String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
+ + " ".repeat(colStart - 1);
+ String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1));
+ sb.append(indent).append(markers);
+
+ // custom message
+ if (customMessage != null && !customMessage.isBlank()) {
+ String offset = " ".repeat(padding + colEnd + PIPE.length() + 1);
+ sb.append(" " + customMessage.replace("\n", "\n" + offset));
+ }
+ sb.append(Colors.RESET).append("\n");
+ }
+ }
+ }
+ return sb.toString();
+ } catch (Exception e) {
+ return null;
+ }
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj)
+ return true;
+ if (obj == null || getClass() != obj.getClass())
+ return false;
+ LJDiagnostic other = (LJDiagnostic) obj;
+ return title.equals(other.title) && message.equals(other.message)
+ && ((file == null && other.file == null) || (file != null && file.equals(other.file)))
+ && ((position == null && other.position == null)
+ || (position != null && position.equals(other.position)));
+ }
+
+ @Override
+ public int hashCode() {
+ int result = title.hashCode();
+ result = 31 * result + message.hashCode();
+ result = 31 * result + (file != null ? file.hashCode() : 0);
+ result = 31 * result + (position != null ? position.hashCode() : 0);
+ return result;
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java
deleted file mode 100644
index 02a6d315..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java
+++ /dev/null
@@ -1,117 +0,0 @@
-package liquidjava.diagnostics;
-
-import java.util.ArrayList;
-import java.util.HashMap;
-
-import liquidjava.diagnostics.errors.LJError;
-import liquidjava.diagnostics.warnings.LJWarning;
-import liquidjava.processor.context.PlacementInCode;
-
-/**
- * Singleton class to store diagnostics information (errors, warnings, translation map) during the verification process
- *
- * @see LJError
- * @see LJWarning
- */
-public class LJDiagnostics {
- private static LJDiagnostics instance;
-
- private ArrayList errors;
- private ArrayList warnings;
- private HashMap translationMap;
-
- private LJDiagnostics() {
- this.errors = new ArrayList<>();
- this.warnings = new ArrayList<>();
- this.translationMap = new HashMap<>();
- }
-
- public static LJDiagnostics getInstance() {
- if (instance == null)
- instance = new LJDiagnostics();
- return instance;
- }
-
- public static LJDiagnostics add(LJError error) {
- LJDiagnostics instance = getInstance();
- instance.addError(error);
- return instance;
- }
-
- public static LJDiagnostics add(LJWarning warning) {
- LJDiagnostics instance = getInstance();
- instance.addWarning(warning);
- return instance;
- }
-
- public static LJDiagnostics add(HashMap map) {
- LJDiagnostics instance = getInstance();
- instance.setTranslationMap(map);
- return instance;
- }
-
- public void addError(LJError error) {
- this.errors.add(error);
- }
-
- public void addWarning(LJWarning warning) {
- this.warnings.add(warning);
- }
-
- public void setTranslationMap(HashMap map) {
- this.translationMap = map;
- }
-
- public boolean foundError() {
- return !this.errors.isEmpty();
- }
-
- public boolean foundWarning() {
- return !this.warnings.isEmpty();
- }
-
- public ArrayList getErrors() {
- return this.errors;
- }
-
- public ArrayList getWarnings() {
- return this.warnings;
- }
-
- public HashMap getTranslationMap() {
- return this.translationMap;
- }
-
- 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();
- this.translationMap.clear();
- }
-
- @Override
- public String toString() {
- 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();
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java
new file mode 100644
index 00000000..01f96c77
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java
@@ -0,0 +1,17 @@
+package liquidjava.diagnostics;
+
+import java.util.HashMap;
+
+import liquidjava.processor.context.PlacementInCode;
+
+/**
+ * Translation table mapping variable names to their placement in code
+ *
+ * @see HashMap
+ * @see PlacementInCode
+ */
+public class TranslationTable extends HashMap {
+ public TranslationTable() {
+ super();
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java
new file mode 100644
index 00000000..d8516f91
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java
@@ -0,0 +1,21 @@
+package liquidjava.diagnostics.errors;
+
+import liquidjava.diagnostics.TranslationTable;
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * Error indicating that the arguments provided to a function or method do not match the expected parameters either in
+ * number or type of arguments
+ *
+ * @see LJError
+ */
+public class ArgumentMismatchError extends LJError {
+
+ public ArgumentMismatchError(String message) {
+ super("Argument Mismatch Error", message, null, null);
+ }
+
+ public ArgumentMismatchError(String message, SourcePosition position, TranslationTable translationTable) {
+ super("Argument Mismatch Error", message, position, translationTable);
+ }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
index 7f885e45..94e007f0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
@@ -1,5 +1,7 @@
package liquidjava.diagnostics.errors;
+import spoon.reflect.cu.SourcePosition;
+
/**
* Custom error with an arbitrary message
*
@@ -8,11 +10,10 @@
public class CustomError extends LJError {
public CustomError(String message) {
- super("Found Error", message, null);
+ super("Error", message, null, null);
}
- @Override
- public String toString() {
- return super.toString(null);
+ public CustomError(String message, SourcePosition position) {
+ super("Error", message, position, null);
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java
deleted file mode 100644
index 7d04e28d..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java
+++ /dev/null
@@ -1,30 +0,0 @@
-package liquidjava.diagnostics.errors;
-
-import liquidjava.rj_language.Predicate;
-import spoon.reflect.declaration.CtElement;
-
-/**
- * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments)
- *
- * @see LJError
- */
-public class GhostInvocationError extends LJError {
-
- private Predicate expected;
-
- public GhostInvocationError(CtElement element, Predicate expected) {
- super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element);
- this.expected = expected;
- }
-
- public Predicate getExpected() {
- return expected;
- }
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Expected: ").append(expected.toString()).append("\n");
- return super.toString(sb.toString());
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
index af5f05c6..ac04737d 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
@@ -11,11 +11,7 @@ public class IllegalConstructorTransitionError extends LJError {
public IllegalConstructorTransitionError(CtElement element) {
super("Illegal Constructor Transition Error",
- "Found constructor with 'from' state (should only have a 'to' state)", element);
- }
-
- @Override
- public String toString() {
- return super.toString(null);
+ "Found constructor with 'from' state: constructors should only have a 'to' state",
+ element.getPosition(), null);
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java
index 02b41265..cc14bacb 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java
@@ -1,6 +1,6 @@
package liquidjava.diagnostics.errors;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that a refinement is invalid (e.g., not a boolean expression)
@@ -9,21 +9,14 @@
*/
public class InvalidRefinementError extends LJError {
- private String refinement;
+ private final String refinement;
- public InvalidRefinementError(String message, CtElement element, String refinement) {
- super("Invalid Refinement", message, element);
+ public InvalidRefinementError(SourcePosition position, String message, String refinement) {
+ super("Invalid Refinement", message, position, null);
this.refinement = refinement;
}
public String getRefinement() {
return refinement;
}
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Refinement: ").append(refinement).append("\n");
- return super.toString(sb.toString());
- }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
index 6e92057f..66ff9fd2 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
@@ -1,67 +1,28 @@
package liquidjava.diagnostics.errors;
-import liquidjava.diagnostics.ErrorPosition;
-import liquidjava.utils.Utils;
+import liquidjava.diagnostics.LJDiagnostic;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.Colors;
import spoon.reflect.cu.SourcePosition;
-import spoon.reflect.declaration.CtElement;
/**
* Base class for all LiquidJava errors
*/
-public abstract class LJError extends Exception {
+public abstract class LJError extends LJDiagnostic {
- private String title;
- private String message;
- private CtElement element;
- private ErrorPosition position;
- private SourcePosition location;
+ private final TranslationTable translationTable;
- public LJError(String title, String message, CtElement element) {
- super(message);
- this.title = title;
- this.message = message;
- this.element = element;
- try {
- this.location = element.getPosition();
- this.position = ErrorPosition.fromSpoonPosition(element.getPosition());
- } catch (Exception e) {
- this.location = null;
- this.position = null;
- }
+ public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) {
+ this(title, message, pos, translationTable, null);
}
- public String getTitle() {
- return title;
+ public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable,
+ String customMessage) {
+ super(title, message, pos, Colors.BOLD_RED, customMessage);
+ this.translationTable = translationTable != null ? translationTable : new TranslationTable();
}
- public String getMessage() {
- return message;
- }
-
- public CtElement getElement() {
- return element;
- }
-
- public ErrorPosition getPosition() {
- return position;
- }
-
- public SourcePosition getLocation() {
- return location;
- }
-
- @Override
- public abstract String toString();
-
- public String toString(String extra) {
- StringBuilder sb = new StringBuilder();
- sb.append(title).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@"))
- .append("\n\n");
- sb.append(message).append("\n");
- if (extra != null)
- sb.append(extra).append("\n");
- sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "")
- .append("\n");
- return sb.toString();
+ public TranslationTable getTranslationTable() {
+ return translationTable;
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
index 77d1ab1f..1a2c260a 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
@@ -1,6 +1,8 @@
package liquidjava.diagnostics.errors;
-import spoon.reflect.declaration.CtElement;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.utils.Utils;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that an element referenced in a refinement was not found
@@ -9,12 +11,24 @@
*/
public class NotFoundError extends LJError {
- public NotFoundError(String message, CtElement element) {
- super("Not Found Error", message, element);
+ private final String name;
+ private final String kind; // "Variable" | "Ghost" | "Alias"
+
+ public NotFoundError(String name, String kind) {
+ this(null, name, kind, null);
+ }
+
+ public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) {
+ super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable);
+ this.name = Utils.getSimpleName(name);
+ this.kind = kind;
+ }
+
+ public String getName() {
+ return name;
}
- @Override
- public String toString() {
- return super.toString(null);
+ public String getKind() {
+ return kind;
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
index fc4b31f1..de40bd7f 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -1,9 +1,9 @@
package liquidjava.diagnostics.errors;
-import liquidjava.rj_language.Predicate;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.Expression;
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
-import liquidjava.utils.Utils;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that a refinement constraint either was violated or cannot be proven
@@ -12,20 +12,22 @@
*/
public class RefinementError extends LJError {
- private Predicate expected;
- private ValDerivationNode found;
+ private final ValDerivationNode expected;
+ private final ValDerivationNode found;
- public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) {
- super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element);
+ public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
+ TranslationTable translationTable, String customMessage) {
+ super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
+ position, translationTable, customMessage);
this.expected = expected;
this.found = found;
}
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Expected: ").append(Utils.stripParens(expected.toString())).append("\n");
- sb.append("Found: ").append(found.getValue());
- return super.toString(sb.toString());
+ public ValDerivationNode getExpected() {
+ return expected;
+ }
+
+ public ValDerivationNode getFound() {
+ return found;
}
}
\ No newline at end of file
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
index 1f714cb2..b8e262fa 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
@@ -1,7 +1,8 @@
package liquidjava.diagnostics.errors;
-import liquidjava.rj_language.Predicate;
-import spoon.reflect.declaration.CtElement;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.Expression;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that two disjoint states were found in a state refinement
@@ -10,30 +11,16 @@
*/
public class StateConflictError extends LJError {
- private Predicate predicate;
- private String className;
+ private final String state;;
- public StateConflictError(CtElement element, Predicate predicate, String className) {
+ public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) {
super("State Conflict Error",
- "Found multiple disjoint states in state transition โ State transition can only go to one state of each state set",
- element);
- this.predicate = predicate;
- this.className = className;
+ "Found multiple disjoint states in state transition: state transition can only go to one state of each state set",
+ position, translationTable);
+ this.state = state.toString();
}
- public Predicate getPredicate() {
- return predicate;
- }
-
- public String getClassName() {
- return className;
- }
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Class: ").append(className).append("\n");
- sb.append("Predicate: ").append(predicate.toString());
- return super.toString(sb.toString());
+ public String getState() {
+ return state;
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
index 5810946d..976508cf 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -1,8 +1,8 @@
package liquidjava.diagnostics.errors;
-import java.util.Arrays;
-
-import spoon.reflect.declaration.CtElement;
+import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.Expression;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that a state refinement transition was violated
@@ -11,37 +11,23 @@
*/
public class StateRefinementError extends LJError {
- private final String method;
- private final String[] expected;
+ private final String expected;
private final String found;
- public StateRefinementError(CtElement element, String method, String[] expected, String found) {
- super("State Refinement Error", "State refinement transition violation", element);
- this.method = method;
- this.expected = expected;
- this.found = found;
- }
-
- public String getMethod() {
- return method;
+ public StateRefinementError(SourcePosition position, Expression expected, Expression found,
+ TranslationTable translationTable, String customMessage) {
+ super("State Refinement Error",
+ String.format("Expected state %s but found %s", expected.toString(), found.toString()), position,
+ translationTable, customMessage);
+ this.expected = expected.toString();
+ this.found = found.toString();
}
- public String[] getExpected() {
+ public String getExpected() {
return expected;
}
public String getFound() {
return found;
}
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Method: ").append(method).append("\n");
- sb.append("Expected: ");
- Arrays.stream(expected).forEach(s -> sb.append(s).append(", "));
- sb.append("\n");
- sb.append("Found: ").append(found);
- return super.toString(sb.toString());
- }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java
index ba679cc6..aac27123 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java
@@ -1,6 +1,6 @@
package liquidjava.diagnostics.errors;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
/**
* Error indicating that the syntax of a refinement is invalid
@@ -9,25 +9,18 @@
*/
public class SyntaxError extends LJError {
- private String refinement;
+ private final String refinement;
public SyntaxError(String message, String refinement) {
this(message, null, refinement);
}
- public SyntaxError(String message, CtElement element, String refinement) {
- super("Syntax Error", message, element);
+ public SyntaxError(String message, SourcePosition pos, String refinement) {
+ super("Syntax Error", message, pos, null);
this.refinement = refinement;
}
public String getRefinement() {
return refinement;
}
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Invalid syntax in refinement: ").append(refinement);
- return super.toString(sb.toString());
- }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java
new file mode 100644
index 00000000..22e5917d
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/CustomWarning.java
@@ -0,0 +1,20 @@
+package liquidjava.diagnostics.warnings;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * Custom warning with a message
+ *
+ * @see LJWarning
+ */
+public class CustomWarning extends LJWarning {
+
+ public CustomWarning(SourcePosition position, String message) {
+ super(message, position);
+ }
+
+ public CustomWarning(String message) {
+ super(message, null);
+ }
+
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java
index 6a4eef29..356542f0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java
@@ -1,6 +1,6 @@
package liquidjava.diagnostics.warnings;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
/**
* Warning indicating that a class referenced in an external refinement was not found
@@ -9,21 +9,14 @@
*/
public class ExternalClassNotFoundWarning extends LJWarning {
- private String className;
+ private final String className;
- public ExternalClassNotFoundWarning(CtElement element, String className) {
- super("Class in external refinement not found", element);
+ public ExternalClassNotFoundWarning(SourcePosition position, String message, String className) {
+ super(message, position);
this.className = className;
}
public String getClassName() {
return className;
}
-
- @Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Class: ").append(className);
- return super.toString(sb.toString());
- }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java
index eee01505..c9f573ae 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java
@@ -1,6 +1,6 @@
package liquidjava.diagnostics.warnings;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
/**
* Warning indicating that a method referenced in an external refinement was not found
@@ -9,13 +9,16 @@
*/
public class ExternalMethodNotFoundWarning extends LJWarning {
- private String methodName;
- private String className;
+ private final String methodName;
+ private final String className;
+ private final String[] overloads;
- public ExternalMethodNotFoundWarning(CtElement element, String methodName, String className) {
- super("Method in external refinement not found", element);
+ public ExternalMethodNotFoundWarning(SourcePosition position, String message, String methodName, String className,
+ String[] overloads) {
+ super(message, position);
this.methodName = methodName;
this.className = className;
+ this.overloads = overloads;
}
public String getMethodName() {
@@ -26,11 +29,12 @@ public String getClassName() {
return className;
}
+ public String[] getOverloads() {
+ return overloads;
+ }
+
@Override
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("Class: ").append(className).append("\n");
- sb.append("Method: ").append(methodName);
- return super.toString(sb.toString());
+ public String getDetails() {
+ return overloads.length > 0 ? String.format("Available overloads:\n %s", String.join("\n ", overloads)) : "";
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java
index 7cf59dd9..5f5f0633 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java
@@ -1,60 +1,15 @@
package liquidjava.diagnostics.warnings;
-import liquidjava.diagnostics.ErrorPosition;
-import liquidjava.utils.Utils;
+import liquidjava.diagnostics.Colors;
+import liquidjava.diagnostics.LJDiagnostic;
import spoon.reflect.cu.SourcePosition;
-import spoon.reflect.declaration.CtElement;
/**
* Base class for all LiquidJava warnings
*/
-public abstract class LJWarning {
+public abstract class LJWarning extends LJDiagnostic {
- private String message;
- private CtElement element;
- private ErrorPosition position;
- private SourcePosition location;
-
- public LJWarning(String message, CtElement element) {
- this.message = message;
- this.element = element;
- try {
- this.location = element.getPosition();
- this.position = ErrorPosition.fromSpoonPosition(element.getPosition());
- } catch (Exception e) {
- // This warning is from a generated part of the source code, so no precise position is provided
- this.location = null;
- this.position = null;
- }
- }
-
- public String getMessage() {
- return message;
- }
-
- public CtElement getElement() {
- return element;
- }
-
- public ErrorPosition getPosition() {
- return position;
- }
-
- public SourcePosition getLocation() {
- return location;
- }
-
- @Override
- public abstract String toString();
-
- public String toString(String extra) {
- StringBuilder sb = new StringBuilder();
- sb.append(message).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@"))
- .append("\n\n");
- if (extra != null)
- sb.append(extra).append("\n");
- sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "")
- .append("\n");
- return sb.toString();
+ public LJWarning(String message, SourcePosition pos) {
+ super("Warning", message, pos, Colors.BOLD_YELLOW, null);
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
index 46069f40..ba8d268a 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java
@@ -3,7 +3,8 @@
import java.util.ArrayList;
import java.util.List;
-import liquidjava.diagnostics.ErrorEmitter;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
import liquidjava.processor.ann_generation.FieldGhostsGeneration;
import liquidjava.processor.context.Context;
import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker;
@@ -18,11 +19,10 @@ public class RefinementProcessor extends AbstractProcessor {
List visitedPackages = new ArrayList<>();
Factory factory;
- ErrorEmitter errorEmitter;
+ Diagnostics diagnostics = Diagnostics.getInstance();
- public RefinementProcessor(Factory factory, ErrorEmitter ee) {
+ public RefinementProcessor(Factory factory) {
this.factory = factory;
- errorEmitter = ee;
}
@Override
@@ -32,16 +32,22 @@ public void process(CtPackage pkg) {
Context c = Context.getInstance();
c.reinitializeAllContext();
- pkg.accept(new FieldGhostsGeneration(c, factory, errorEmitter)); // generate annotations for field ghosts
-
- // void spoon.reflect.visitor.CtVisitable.accept(CtVisitor arg0)
- pkg.accept(new ExternalRefinementTypeChecker(c, factory, errorEmitter));
-
- pkg.accept(new MethodsFirstChecker(c, factory, errorEmitter)); // double passing idea (instead of headers)
-
- pkg.accept(new RefinementTypeChecker(c, factory, errorEmitter));
- if (errorEmitter.foundError())
- return;
+ try {
+ // process types in this package only, not sub-packages
+ // first pass: gather refinements
+ pkg.getTypes().forEach(type -> {
+ type.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts
+ type.accept(new ExternalRefinementTypeChecker(c, factory)); // process external refinements
+ type.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers)
+ });
+
+ // second pass: check refinements
+ pkg.getTypes().forEach(type -> {
+ type.accept(new RefinementTypeChecker(c, factory));
+ });
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
}
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java b/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java
deleted file mode 100644
index 43fa8393..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java
+++ /dev/null
@@ -1,27 +0,0 @@
-package liquidjava.processor;
-
-import spoon.Launcher;
-
-public class TestInsideClasses {
- public static void main(String[] args) {
-
- Launcher launcher = new Launcher();
- launcher.getEnvironment().setComplianceLevel(8);
- launcher.run();
-
- // final Factory factory = launcher.getFactory();
- // RefinedVariable vi2 = new Variable("a",factory.Type().INTEGER_PRIMITIVE, new Predicate("a >
- // 0"));
- // CtTypeReference intt = factory.Type().INTEGER_PRIMITIVE;
- // List> l = new ArrayList<>();
- // l.add(intt);
- // GhostState s = new GhostState("green", l, intt, "A");
- // GhostState ss = new GhostState("yellow", l, intt, "A");
- // GhostState sss = new GhostState("red", l, intt, "A");
- // List gh = new ArrayList<>();
- // gh.add(s);gh.add(ss);gh.add(sss);
- // Predicate p = new Predicate("green(this) && red(this) == iio && u(3)");
- // System.out.println(p.getVariableNames());
-
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java
index 35daad11..152488a8 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java
@@ -32,7 +32,7 @@ public String toString() {
String qualType = type.getQualifiedName();
String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType;
return String.format("%-20s %s %s", "โ" + name + ":" + simpleType + ",", refinement.toString(),
- next != null ? " => \n" + next.toString() : "");
+ next != null ? " => \n" + next : "");
} else
return String.format("%-20s %s", "", refinement.toString());
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java
index dbe672f5..10ad84e6 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java
@@ -1,6 +1,5 @@
package liquidjava.processor.ann_generation;
-import liquidjava.diagnostics.ErrorEmitter;
import liquidjava.processor.context.Context;
import liquidjava.specification.Ghost;
import spoon.reflect.declaration.*;
@@ -11,12 +10,10 @@
public class FieldGhostsGeneration extends CtScanner {
Context context;
Factory factory;
- ErrorEmitter errorEmitter;
- public FieldGhostsGeneration(Context c, Factory fac, ErrorEmitter errorEmitter) {
- this.context = c;
- this.factory = fac;
- this.errorEmitter = errorEmitter;
+ public FieldGhostsGeneration(Context context, Factory factory) {
+ this.context = context;
+ this.factory = factory;
}
public Context getContext() {
@@ -29,16 +26,12 @@ public Factory getFactory() {
@Override
public void visitCtClass(CtClass ctClass) {
- if (errorEmitter.foundError()) {
- return;
- }
-
ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int"))
.forEach(fld -> {
- CtTypeReference fld_type = fld.getType();
- CtAnnotation gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
- gen_ann.addValue("value", fld_type.getSimpleName() + " " + fld.getSimpleName());
- ctClass.addAnnotation(gen_ann);
+ CtTypeReference fldType = fld.getType();
+ CtAnnotation genAnn = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
+ genAnn.addValue("value", fldType.getSimpleName() + " " + fld.getSimpleName());
+ ctClass.addAnnotation(genAnn);
});
super.visitCtClass(ctClass);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
index cb218d7e..a9838440 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java
@@ -1,33 +1,22 @@
package liquidjava.processor.context;
import java.util.ArrayList;
-import java.util.HashMap;
import java.util.List;
-import java.util.Map;
-
-import liquidjava.diagnostics.ErrorEmitter;
import liquidjava.processor.facade.AliasDTO;
import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.ast.Expression;
-import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.utils.Utils;
-import spoon.reflect.declaration.CtElement;
import spoon.reflect.factory.Factory;
import spoon.reflect.reference.CtTypeReference;
public class AliasWrapper {
- private String name;
- private List> varTypes;
- private List varNames;
- private Predicate expression;
- // private Context context;
-
- private String newAliasFormat = "#alias_%s_%d";
+ private final String name;
+ private final List> varTypes;
+ private final List varNames;
+ private final Predicate expression;
- public AliasWrapper(AliasDTO a, Factory factory, String wILD_VAR, Context context2, String klass, String path) {
+ public AliasWrapper(AliasDTO a, Factory factory, String klass, String path) {
name = a.getName();
expression = new Predicate(a.getExpression());
-
varTypes = new ArrayList<>();
varNames = a.getVarNames();
for (String s : a.getVarTypes()) {
@@ -49,71 +38,10 @@ public List getVarNames() {
}
public Predicate getClonedPredicate() {
- return (Predicate) expression.clone();
- }
-
- public Expression getNewExpression(List newNames) {
- Predicate expr = getClonedPredicate();
- for (int i = 0; i < newNames.size(); i++) {
- expr = expr.substituteVariable(varNames.get(i), newNames.get(i));
- }
- return expr.getExpression().clone();
- }
-
- public Predicate getPremises(List list, List newNames, CtElement elem, ErrorEmitter ee)
- throws ParsingException {
- List invocationPredicates = getPredicatesFromExpression(list, elem, ee);
- Predicate prem = new Predicate();
- for (int i = 0; i < invocationPredicates.size(); i++) {
- prem = Predicate.createConjunction(prem,
- Predicate.createEquals(Predicate.createVar(newNames.get(i)), invocationPredicates.get(i)));
- }
- return prem.clone();
- }
-
- private List getPredicatesFromExpression(List list, CtElement elem, ErrorEmitter ee)
- throws ParsingException {
- List lp = new ArrayList<>();
- for (String e : list)
- lp.add(new Predicate(e, elem, ee));
-
- return lp;
- }
-
- public List getNewVariables(Context context) {
- List n = new ArrayList<>();
- for (int i = 0; i < varNames.size(); i++)
- n.add(String.format(newAliasFormat, varNames.get(i), context.getCounter()));
- return n;
- }
-
- public Map> getTypes(List names) {
- Map> m = new HashMap<>();
- for (int i = 0; i < names.size(); i++) {
- m.put(names.get(i), varTypes.get(i));
- }
- return m;
+ return expression.clone();
}
public AliasDTO createAliasDTO() {
return new AliasDTO(name, varTypes, varNames, expression.getExpression());
}
-
- // public Expression getSubstitutedExpression(List newNames) {
- // return null;
- // }
- //
-
- // TypeKeyword tk;
- // AliasName name;
- //
- // ParenthesisLeft pl;
- // Type type;
- // Var var;
- // ParenthesisRight rl;
- //
- // BraceLeft bl;
- // Expression e;
- // BraceRight br;
-
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
index a09fb0e4..ca4d68e8 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
@@ -10,7 +10,7 @@ public class Context {
private List ctxFunctions;
private List ctxSpecificVars;
- private List ctxGlobalVars;
+ private final List ctxGlobalVars;
private List ghosts;
private Map> classStates;
@@ -24,9 +24,7 @@ private Context() {
ctxVars.add(new ArrayList<>());
ctxFunctions = new ArrayList<>();
ctxSpecificVars = new ArrayList<>();
- // globals
ctxGlobalVars = new ArrayList<>();
- // ctxGlobalFunctions = new ArrayList<>();
alias = new ArrayList<>();
ghosts = new ArrayList<>();
@@ -34,7 +32,6 @@ private Context() {
counter = 0;
}
- // SINGLETON
public static Context getInstance() {
if (instance == null)
instance = new Context();
@@ -44,11 +41,7 @@ public static Context getInstance() {
public void reinitializeContext() {
ctxVars = new Stack<>();
ctxVars.add(new ArrayList<>()); // global vars
- // ctxFunctions = new ArrayList<>();
ctxSpecificVars = new ArrayList<>();
- // alias = new ArrayList<>();
- // ghosts = new ArrayList<>();
- // counter = 0;
}
public void reinitializeAllContext() {
@@ -95,12 +88,6 @@ public Map> getContext() {
}
// ---------------------- Global variables ----------------------
- public void addGlobalVariableToContext(String simpleName, CtTypeReference type, Predicate c) {
- RefinedVariable vi = new Variable(simpleName, type, c);
- ctxGlobalVars.add(vi);
- vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
- }
-
public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference type, Predicate c) {
RefinedVariable vi = new Variable(simpleName, location, type, c);
vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
@@ -109,7 +96,6 @@ public void addGlobalVariableToContext(String simpleName, String location, CtTyp
// ---------------------- Add variables and instances ----------------------
public void addVarToContext(RefinedVariable var) {
- // if(!hasVariable(var.getName()))
ctxVars.peek().add(var);
CtTypeReference type = var.getType();
var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
@@ -183,27 +169,15 @@ public boolean hasVariable(String name) {
return getVariableByName(name) != null;
}
- public String allVariablesToString() {
- StringBuilder sb = new StringBuilder();
- for (List l : ctxVars) {
- for (RefinedVariable var : l) {
- sb.append(var.toString() + "; ");
- }
- }
- return sb.toString();
- }
-
/**
* Lists all variables inside the stack
*
- * @return
+ * @return list of all variables
*/
public List getAllVariables() {
List lvi = new ArrayList<>();
for (List l : ctxVars) {
- for (RefinedVariable var : l) {
- lvi.add(var);
- }
+ lvi.addAll(l);
}
return lvi;
}
@@ -211,11 +185,11 @@ public List getAllVariables() {
public List getAllVariablesWithSupertypes() {
List lvi = new ArrayList<>();
for (RefinedVariable rv : getAllVariables()) {
- if (rv.getSuperTypes().size() > 0)
+ if (!rv.getSuperTypes().isEmpty())
lvi.add(rv);
}
for (RefinedVariable rv : ctxSpecificVars) {
- if (rv.getSuperTypes().size() > 0)
+ if (!rv.getSuperTypes().isEmpty())
lvi.add(rv);
}
return lvi;
@@ -298,18 +272,6 @@ public void addFunctionToContext(RefinedFunction f) {
ctxFunctions.add(f);
}
- public RefinedFunction getFunction(String name, String target) {
- for (RefinedFunction fi : ctxFunctions) {
- if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target))
- return fi;
- }
- // for(RefinedFunction fi: ctxGlobalFunctions) {
- // if(fi.getName().equals(name) && fi.getTargetClass().equals(target))
- // return fi;
- // }
- return null;
- }
-
public RefinedFunction getFunction(String name, String target, int size) {
for (RefinedFunction fi : ctxFunctions) {
if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)
@@ -333,14 +295,6 @@ public void addGhostFunction(GhostFunction gh) {
ghosts.add(gh);
}
- public boolean hasGhost(String name) {
- for (GhostFunction g : ghosts) {
- if (g.matches(name))
- return true;
- }
- return false;
- }
-
public List getGhosts() {
return ghosts;
}
@@ -387,13 +341,10 @@ public String toString() {
for (List l : ctxVars) {
sb.append("{");
for (RefinedVariable var : l) {
- sb.append(var.toString() + "; ");
+ sb.append(var.toString()).append("; ");
}
sb.append("}\n");
}
- // sb.append("\n############Global Functions:############\n");
- // for(RefinedFunction f : ctxGlobalFunctions)
- // sb.append(f.toString());
sb.append("\n############Functions:############\n");
for (RefinedFunction f : ctxFunctions)
sb.append(f.toString());
@@ -406,10 +357,5 @@ public String toString() {
public Variable getVariableFromInstance(VariableInstance vi) {
return vi.getParent().orElse(null);
- // for(List lv: ctxVars)
- // for(RefinedVariable v: lv)
- // if(v instanceof Variable && ((Variable)v).hasInstance(vi))
- // return (Variable)v;
- // return null;
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java
index 769f4680..50a4f548 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java
@@ -9,57 +9,55 @@
public class GhostFunction {
- private String name;
- private List> param_types;
- private CtTypeReference return_type;
- private String prefix;
+ private final String name;
+ private final List> paramTypes;
+ private final CtTypeReference returnType;
+ private final String prefix;
public GhostFunction(GhostDTO f, Factory factory, String prefix) {
String klass = this.getParentClassName(prefix);
- this.name = f.getName();
- this.return_type = Utils.getType(f.getReturn_type().equals(klass) ? prefix : f.getReturn_type(), factory);
- this.param_types = new ArrayList<>();
+ this.name = f.name();
+ this.returnType = Utils.getType(f.returnType().equals(klass) ? prefix : f.returnType(), factory);
+ this.paramTypes = new ArrayList<>();
this.prefix = prefix;
- for (String t : f.getParam_types()) {
- this.param_types.add(Utils.getType(t.equals(klass) ? prefix : t, factory));
+ for (String t : f.paramTypes()) {
+ this.paramTypes.add(Utils.getType(t.equals(klass) ? prefix : t, factory));
}
}
- public GhostFunction(String name, List param_types, CtTypeReference return_type, Factory factory,
+ public GhostFunction(String name, List paramTypes, CtTypeReference returnType, Factory factory,
String prefix) {
String klass = this.getParentClassName(prefix);
- String type = return_type.toString().equals(klass) ? prefix : return_type.toString();
+ String type = returnType.toString().equals(klass) ? prefix : returnType.toString();
this.name = name;
- this.return_type = Utils.getType(type, factory);
- this.param_types = new ArrayList<>();
+ this.returnType = Utils.getType(type, factory);
+ this.paramTypes = new ArrayList<>();
this.prefix = prefix;
- for (int i = 0; i < param_types.size(); i++) {
- String mType = param_types.get(i).toString();
- this.param_types.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory));
+ for (String mType : paramTypes) {
+ this.paramTypes.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory));
}
}
- protected GhostFunction(String name, List> list, CtTypeReference return_type, String prefix) {
+ protected GhostFunction(String name, List> list, CtTypeReference returnType, String prefix) {
this.name = name;
- this.return_type = return_type;
- this.param_types = new ArrayList<>();
- this.param_types = list;
+ this.returnType = returnType;
+ this.paramTypes = list;
this.prefix = prefix;
}
public CtTypeReference getReturnType() {
- return return_type;
+ return returnType;
}
public List> getParametersTypes() {
- return param_types;
+ return paramTypes;
}
public String toString() {
StringBuilder sb = new StringBuilder();
- sb.append("ghost " + return_type.toString() + " " + name + "(");
- for (CtTypeReference t : param_types) {
- sb.append(t.toString() + " ,");
+ sb.append("ghost ").append(returnType.toString()).append(" ").append(name).append("(");
+ for (CtTypeReference t : paramTypes) {
+ sb.append(t.toString()).append(" ,");
}
sb.delete(sb.length() - 2, sb.length());
sb.append(")");
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java
deleted file mode 100644
index 64974bdf..00000000
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java
+++ /dev/null
@@ -1,28 +0,0 @@
-package liquidjava.processor.context;
-
-import java.util.ArrayList;
-import java.util.List;
-import spoon.reflect.factory.Factory;
-import spoon.reflect.reference.CtTypeReference;
-
-public class GhostParentState extends GhostFunction {
-
- private ArrayList states;
-
- public GhostParentState(String name, List params, CtTypeReference ret, Factory factory, String prefix) {
- super(name, params, ret, factory, prefix);
- states = new ArrayList<>();
- }
-
- public void addState(GhostState s) {
- states.add(s);
- }
-
- public GhostState getFirstState() {
- return states.get(0);
- }
-
- public ArrayList getStates() {
- return states;
- }
-}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
index 3cdcacb7..121f0339 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java
@@ -9,8 +9,8 @@ public class GhostState extends GhostFunction {
private GhostFunction parent;
private Predicate refinement;
- public GhostState(String name, List> list, CtTypeReference return_type, String prefix) {
- super(name, list, return_type, prefix);
+ public GhostState(String name, List> list, CtTypeReference returnType, String prefix) {
+ super(name, list, returnType, prefix);
}
public void setGhostParent(GhostFunction parent) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java
index 795e9815..45ac6c68 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java
@@ -6,6 +6,7 @@ public class ObjectState {
Predicate from;
Predicate to;
+ String message;
public ObjectState() {
}
@@ -15,6 +16,12 @@ public ObjectState(Predicate from, Predicate to) {
this.to = to;
}
+ public ObjectState(Predicate from, Predicate to, String message) {
+ this.from = from;
+ this.to = to;
+ this.message = message;
+ }
+
public void setFrom(Predicate from) {
this.from = from;
}
@@ -39,8 +46,16 @@ public Predicate getTo() {
return to != null ? to : new Predicate();
}
+ public String getMessage() {
+ return message;
+ }
+
+ public void setMessage(String message) {
+ this.message = message;
+ }
+
public ObjectState clone() {
- return new ObjectState(from.clone(), to.clone());
+ return new ObjectState(from.clone(), to.clone(), message);
}
@Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
index 2a8f90af..3400f5f7 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java
@@ -7,12 +7,12 @@
import spoon.reflect.declaration.CtElement;
public class PlacementInCode {
- private String text;
- private SourcePosition position;
+ private final String text;
+ private final SourcePosition position;
- private PlacementInCode(String t, SourcePosition s) {
- this.text = t;
- this.position = s;
+ private PlacementInCode(String text, SourcePosition pos) {
+ this.text = text;
+ this.position = pos;
}
public String getText() {
@@ -23,24 +23,16 @@ public SourcePosition getPosition() {
return position;
}
- public void setText(String text) {
- this.text = text;
- }
-
- public void setPosition(SourcePosition position) {
- this.position = position;
- }
-
public static PlacementInCode createPlacement(CtElement elem) {
CtElement elemCopy = elem.clone();
// cleanup annotations
- if (elem.getAnnotations().size() > 0) {
+ if (!elem.getAnnotations().isEmpty()) {
for (CtAnnotation a : elem.getAnnotations()) {
elemCopy.removeAnnotation(a);
}
}
// cleanup comments
- if (elem.getComments().size() > 0) {
+ if (!elem.getComments().isEmpty()) {
for (CtComment a : elem.getComments()) {
elemCopy.removeComment(a);
}
@@ -49,13 +41,6 @@ public static PlacementInCode createPlacement(CtElement elem) {
return new PlacementInCode(elemText, elem.getPosition());
}
- public String getSimplePosition() {
- if (position.getFile() == null) {
- return "No position provided. Possibly asking for generated code";
- }
- return position.getFile().getName() + ":" + position.getLine() + ", " + position.getColumn();
- }
-
public String toString() {
if (position.getFile() == null) {
return "No position provided. Possibly asking for generated code";
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java
index a597fe24..2aa03989 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java
@@ -8,6 +8,7 @@ public abstract class Refined {
private String name; // y
private CtTypeReference type; // int
private Predicate refinement; // 9 <= y && y <= 100
+ private String message;
public Refined() {
}
@@ -44,6 +45,14 @@ public Predicate getRefinement() {
return new Predicate();
}
+ public String getMessage() {
+ return message;
+ }
+
+ public void setMessage(String message) {
+ this.message = message;
+ }
+
public Predicate getRenamedRefinements(String toReplace) {
return refinement.substituteVariable(name, toReplace);
}
@@ -78,10 +87,9 @@ public boolean equals(Object obj) {
} else if (!name.equals(other.name))
return false;
if (type == null) {
- if (other.type != null)
- return false;
- } else if (!type.equals(other.type))
- return false;
- return true;
+ return other.type == null;
+ } else {
+ return type.equals(other.type);
+ }
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
index 807f4682..f1585cee 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java
@@ -5,11 +5,10 @@
import java.util.Optional;
import liquidjava.rj_language.Predicate;
import spoon.reflect.declaration.CtElement;
-import spoon.reflect.reference.CtTypeReference;
public class RefinedFunction extends Refined {
- private List argRefinements;
+ private final List argRefinements;
private String targetClass;
private List stateChange;
private String signature;
@@ -23,11 +22,6 @@ public List getArguments() {
return argRefinements;
}
- public void addArgRefinements(String varName, CtTypeReference type, Predicate refinement) {
- Variable v = new Variable(varName, type, refinement);
- this.argRefinements.add(v);
- }
-
public void addArgRefinements(Variable vi) {
this.argRefinements.add(vi);
}
@@ -84,24 +78,9 @@ public Predicate getAllRefinements() {
return c;
}
- /**
- * Gives the Predicate for a certain parameter index and regards all the previous parameters' Predicates
- *
- * @param index
- *
- * @return
- */
- public Predicate getRefinementsForParamIndex(int index) {
- Predicate c = new Predicate();
- for (int i = 0; i <= index && i < argRefinements.size(); i++)
- c = Predicate.createConjunction(c, argRefinements.get(i).getRefinement());
- return c;
- }
-
public boolean allRefinementsTrue() {
- boolean t = true;
Predicate p = new Predicate(getRefReturn().getExpression());
- t = t && p.isBooleanTrue();
+ boolean t = p.isBooleanTrue();
for (Variable v : argRefinements) {
p = new Predicate(v.getRefinement().getExpression());
t = t && p.isBooleanTrue();
@@ -122,7 +101,7 @@ public void addStates(ObjectState e) {
}
public boolean hasStateChange() {
- return stateChange.size() > 0;
+ return !stateChange.isEmpty();
}
public List getFromStates() {
@@ -149,7 +128,7 @@ public String toString() {
public int hashCode() {
final int prime = 31;
int result = super.hashCode();
- result = prime * result + ((argRefinements == null) ? 0 : argRefinements.hashCode());
+ result = prime * result + argRefinements.hashCode();
result = prime * result + ((targetClass == null) ? 0 : targetClass.hashCode());
result = prime * result + ((signature == null) ? 0 : signature.hashCode());
return result;
@@ -164,10 +143,7 @@ public boolean equals(Object obj) {
if (getClass() != obj.getClass())
return false;
RefinedFunction other = (RefinedFunction) obj;
- if (argRefinements == null) {
- if (other.argRefinements != null)
- return false;
- } else if (!argRefinements.equals(other.argRefinements))
+ if (!argRefinements.equals(other.argRefinements))
return false;
if (targetClass == null) {
if (other.targetClass != null)
@@ -175,10 +151,9 @@ public boolean equals(Object obj) {
} else if (!targetClass.equals(other.targetClass))
return false;
if (signature == null) {
- if (other.signature != null)
- return false;
- } else if (!signature.equals(other.signature))
- return false;
- return true;
+ return other.signature == null;
+ } else {
+ return signature.equals(other.signature);
+ }
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
index fe3abf11..534f8cfa 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java
@@ -7,7 +7,7 @@
import spoon.reflect.reference.CtTypeReference;
public abstract class RefinedVariable extends Refined {
- private List> supertypes;
+ private final List> supertypes;
private PlacementInCode placementInCode;
public RefinedVariable(String name, CtTypeReference type, Predicate c) {
@@ -60,10 +60,9 @@ public boolean equals(Object obj) {
return false;
RefinedVariable other = (RefinedVariable) obj;
if (supertypes == null) {
- if (other.supertypes != null)
- return false;
- } else if (!supertypes.equals(other.supertypes))
- return false;
- return true;
+ return other.supertypes == null;
+ } else {
+ return supertypes.equals(other.supertypes);
+ }
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java
index ff616db9..13f74cab 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java
@@ -32,7 +32,7 @@ public Variable(String name, String location, CtTypeReference type, Predicate
private void startVariables() {
this.instances = new Stack<>();
- this.instances.push(new ArrayList());
+ this.instances.push(new ArrayList<>());
ifCombiner = new Stack<>();
}
@@ -73,16 +73,11 @@ public void addInstance(VariableInstance vi) {
instances.peek().add(vi);
}
- public void removeLastInstance() {
- if (instances.size() > 0)
- instances.peek().remove(instances.size() - 1);
- }
-
public Optional getLastInstance() {
Stack> backup = new Stack<>();
- while (instances.size() > 0) {
+ while (!instances.isEmpty()) {
List lvi = instances.peek();
- if (lvi.size() > 0) { // last list in stack has a value
+ if (!lvi.isEmpty()) { // last list in stack has a value
reloadFromBackup(backup);
return Optional.of(lvi.get(lvi.size() - 1));
} else {
@@ -94,18 +89,10 @@ public Optional getLastInstance() {
}
private void reloadFromBackup(Stack> backup) {
- while (backup.size() > 0)
+ while (!backup.isEmpty())
instances.add(backup.pop());
}
- public boolean hasInstance(VariableInstance vi) {
- for (List lv : instances)
- for (VariableInstance v : lv)
- if (v.equals(vi))
- return true;
- return false;
- }
-
// IFS
public void newIfCombination() {
ifCombiner.push(new Object[ifelseIndex + 1]);
@@ -167,8 +154,7 @@ else if (has(ifbeforeIndex)) // value before and in else
private boolean has(int index) {
Object o = ifCombiner.peek()[index];
- boolean b = o != null && (o instanceof VariableInstance);
- return b;
+ return (o instanceof VariableInstance);
}
private VariableInstance get(int index) {
@@ -180,7 +166,7 @@ private VariableInstance get(int index) {
*
* @param nName
* @param cond
- * @param ifThen
+ * @param then
*
* @return
*/
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java
index 1a6daf4a..b4bebb0c 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java
@@ -6,7 +6,6 @@
public class VariableInstance extends RefinedVariable {
- // private Predicate state;
private Variable parent;
public VariableInstance(String name, CtTypeReference type, Predicate c) {
@@ -37,13 +36,4 @@ public void setParent(Variable p) {
public Optional getParent() {
return parent == null ? Optional.empty() : Optional.of(parent);
}
-
- // public void setState(Predicate c) {
- // state = c;
- // }
- // public Predicate getState() {
- // return state;
- // }
- //
-
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java
index 8737f572..ca120615 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java
@@ -2,22 +2,24 @@
import java.util.List;
import java.util.stream.Collectors;
+
+import liquidjava.diagnostics.errors.LJError;
import liquidjava.rj_language.ast.Expression;
-import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.rj_language.parsing.RefinementsParser;
+import spoon.reflect.declaration.CtTypeInformation;
import spoon.reflect.reference.CtTypeReference;
public class AliasDTO {
- private String name;
- private List varTypes;
- private List varNames;
+ private final String name;
+ private final List varTypes;
+ private final List varNames;
private Expression expression;
private String ref;
public AliasDTO(String name, List> varTypes, List varNames, Expression expression) {
super();
this.name = name;
- this.varTypes = varTypes.stream().map(m -> m.getQualifiedName()).collect(Collectors.toList());
+ this.varTypes = varTypes.stream().map(CtTypeInformation::getQualifiedName).collect(Collectors.toList());
this.varNames = varNames;
this.expression = expression;
}
@@ -32,7 +34,7 @@ public AliasDTO(String name2, List varTypes2, List varNames2, St
// Parse the alias expression using the given the prefix to ensure ghost names are qualified consistently with
// where the alias is declared or used
- public void parse(String prefix) throws ParsingException {
+ public void parse(String prefix) throws LJError {
if (ref != null) {
this.expression = RefinementsParser.createAST(ref, prefix);
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java
index 6dc9ea82..87dfb5cc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java
@@ -2,28 +2,5 @@
import java.util.List;
-public class GhostDTO {
-
- private String name;
- private List param_types;
- private String return_type;
-
- public GhostDTO(String name, List param_types, String return_type) {
- super();
- this.name = name;
- this.param_types = param_types;
- this.return_type = return_type;
- }
-
- public String getName() {
- return name;
- }
-
- public List getParam_types() {
- return param_types;
- }
-
- public String getReturn_type() {
- return return_type;
- }
+public record GhostDTO(String name, List paramTypes, String returnType) {
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
index 8580135b..154e94d0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -1,20 +1,21 @@
package liquidjava.processor.refinement_checker;
-import java.util.Arrays;
import java.util.List;
import java.util.Optional;
-import java.util.stream.Collectors;
-import liquidjava.diagnostics.ErrorEmitter;
-import liquidjava.diagnostics.ErrorHandler;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning;
+import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning;
import liquidjava.processor.context.Context;
import liquidjava.processor.context.GhostFunction;
import liquidjava.processor.facade.GhostDTO;
import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.rj_language.parsing.RefinementsParser;
import liquidjava.utils.Utils;
+import spoon.reflect.code.CtLiteral;
+import spoon.reflect.declaration.CtAnnotation;
import spoon.reflect.declaration.CtClass;
import spoon.reflect.declaration.CtElement;
import spoon.reflect.declaration.CtField;
@@ -27,34 +28,29 @@
public class ExternalRefinementTypeChecker extends TypeChecker {
String prefix;
- MethodsFunctionsChecker m;
+ Diagnostics diagnostics = Diagnostics.getInstance();
- public ExternalRefinementTypeChecker(Context context, Factory fac, ErrorEmitter errorEmitter) {
- super(context, fac, errorEmitter);
+ public ExternalRefinementTypeChecker(Context context, Factory factory) {
+ super(context, factory);
}
@Override
public void visitCtClass(CtClass ctClass) {
- return;
}
@Override
public void visitCtInterface(CtInterface intrface) {
- if (errorEmitter.foundError())
- return;
-
- Optional externalRefinements = getExternalRefinement(intrface);
- if (externalRefinements.isPresent()) {
- this.prefix = externalRefinements.get();
+ Optional> externalRef = getExternalRefinement(intrface);
+ if (externalRef.isPresent()) {
+ @SuppressWarnings("unchecked")
+ CtLiteral literal = (CtLiteral) externalRef.get().getAllValues().get("value");
+ this.prefix = literal.getValue();
if (!classExists(prefix)) {
- ErrorHandler.printCustomError(intrface, "Could not find class '" + prefix + "'", errorEmitter);
+ String message = String.format("Could not find class '%s'", prefix);
+ diagnostics.add(new ExternalClassNotFoundWarning(externalRef.get().getPosition(), message, prefix));
return;
}
- try {
- getRefinementFromAnnotation(intrface);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ getRefinementFromAnnotation(intrface);
handleStateSetsFromAnnotation(intrface);
super.visitCtInterface(intrface);
}
@@ -62,81 +58,46 @@ public void visitCtInterface(CtInterface intrface) {
@Override
public void visitCtField(CtField f) {
- if (errorEmitter.foundError())
- return;
-
- Optional oc;
- try {
- oc = getRefinementFromAnnotation(f);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ Optional oc = getRefinementFromAnnotation(f);
Predicate c = oc.orElse(new Predicate());
context.addGlobalVariableToContext(f.getSimpleName(), prefix, f.getType(), c);
super.visitCtField(f);
}
public void visitCtMethod(CtMethod method) {
- if (errorEmitter.foundError())
- return;
-
CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration();
- if (targetType == null || !(targetType instanceof CtClass))
+ if (!(targetType instanceof CtClass))
return;
boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName());
if (isConstructor) {
if (!constructorExists(targetType, method)) {
- ErrorHandler.printCustomError(method,
- String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix),
- errorEmitter);
- return;
+ String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(),
+ prefix);
+ String[] overloads = getOverloads(targetType, method);
+ diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+ prefix, overloads));
}
} else {
if (!methodExists(targetType, method)) {
- String matchingNames = targetType.getMethods().stream()
- .filter(m -> m.getSimpleName().equals(method.getSimpleName()))
- .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature()))
- .collect(Collectors.joining("\n "));
-
- StringBuilder sb = new StringBuilder();
- sb.append(String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(),
- method.getSignature(), prefix));
-
- if (!matchingNames.isEmpty()) {
- sb.append("\nAvailable overloads:\n ");
- sb.append(matchingNames);
- }
- ErrorHandler.printCustomError(method, sb.toString(), errorEmitter);
+ String message = String.format("Could not find method '%s %s' for '%s'",
+ method.getType().getSimpleName(), method.getSignature(), prefix);
+ String[] overloads = getOverloads(targetType, method);
+ diagnostics.add(new ExternalMethodNotFoundWarning(method.getPosition(), message, method.getSignature(),
+ prefix, overloads));
return;
}
}
-
MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this);
- try {
- mfc.getMethodRefinements(method, prefix);
- } catch (ParsingException e) {
- return;
- }
+ mfc.getMethodRefinements(method, prefix);
super.visitCtMethod(method);
-
- //
- // System.out.println("visited method external");
}
- protected void getGhostFunction(String value, CtElement element) {
- try {
- // Optional ofd =
- // RefinementParser.parseFunctionDecl(value);
- GhostDTO f = RefinementsParser.getGhostDeclaration(value);
- if (f != null && element.getParent() instanceof CtInterface) {
- GhostFunction gh = new GhostFunction(f, factory, prefix);
- context.addGhostFunction(gh);
- }
-
- } catch (ParsingException e) {
- ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter);
- // e.printStackTrace();
+ protected void getGhostFunction(String value, CtElement element) throws LJError {
+ GhostDTO f = RefinementsParser.getGhostDeclaration(value);
+ if (element.getParent() instanceof CtInterface) {
+ GhostFunction gh = new GhostFunction(f, factory, prefix);
+ context.addGhostFunction(gh);
}
}
@@ -145,7 +106,7 @@ protected Optional createStateGhost(int order, CtElement element)
String klass = Utils.getSimpleName(prefix);
if (klass != null) {
CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE;
- List params = Arrays.asList(klass);
+ List params = List.of(klass);
String name = String.format("state%d", order);
GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix);
return Optional.of(gh);
@@ -206,4 +167,9 @@ private boolean parametersMatch(List targetParams, List refinementParams)
}
return true;
}
+
+ private String[] getOverloads(CtType targetType, CtMethod method) {
+ return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName()))
+ .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())).toArray(String[]::new);
+ }
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
index 92cadcf5..6a148725 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
@@ -3,10 +3,10 @@
import java.util.ArrayList;
import java.util.List;
-import liquidjava.diagnostics.ErrorEmitter;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
import liquidjava.processor.context.Context;
import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
-import liquidjava.rj_language.parsing.ParsingException;
import spoon.reflect.declaration.CtClass;
import spoon.reflect.declaration.CtConstructor;
import spoon.reflect.declaration.CtInterface;
@@ -19,18 +19,16 @@
public class MethodsFirstChecker extends TypeChecker {
MethodsFunctionsChecker mfc;
List visitedClasses;
+ Diagnostics diagnostics = Diagnostics.getInstance();
- public MethodsFirstChecker(Context c, Factory fac, ErrorEmitter errorEmitter) {
- super(c, fac, errorEmitter);
+ public MethodsFirstChecker(Context context, Factory factory) {
+ super(context, factory);
mfc = new MethodsFunctionsChecker(this);
visitedClasses = new ArrayList<>();
}
@Override
public void visitCtClass(CtClass ctClass) {
- if (errorEmitter.foundError())
- return;
-
context.reinitializeContext();
if (visitedClasses.contains(ctClass.getQualifiedName()))
return;
@@ -52,20 +50,25 @@ public void visitCtClass(CtClass ctClass) {
if (ct instanceof CtClass)
visitCtClass((CtClass) ct);
}
+ // first try-catch: process class-level annotations)
+ // errors here should not prevent visiting methods, constructors or fields of the class
try {
getRefinementFromAnnotation(ctClass);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
+ handleStateSetsFromAnnotation(ctClass);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
+ // second try-catch: visit class children (methods, constructors, fields)
+ // errors from one child should not prevent visiting sibling elements
+ try {
+ super.visitCtClass(ctClass);
+ } catch (LJError e) {
+ diagnostics.add(e);
}
- handleStateSetsFromAnnotation(ctClass);
- super.visitCtClass(ctClass);
}
@Override
public void visitCtInterface(CtInterface intrface) {
- if (errorEmitter.foundError())
- return;
-
if (visitedClasses.contains(intrface.getQualifiedName()))
return;
else
@@ -73,41 +76,35 @@ public void visitCtInterface(CtInterface intrface) {
if (getExternalRefinement(intrface).isPresent())
return;
+ // first try-catch: process interface-level annotations
+ // errors here should not prevent visiting the interface's methods
try {
getRefinementFromAnnotation(intrface);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
+ handleStateSetsFromAnnotation(intrface);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
+ // second try-catch: visit interface children (methods)
+ // errors from one child should not prevent visiting sibling methods
+ try {
+ super.visitCtInterface(intrface);
+ } catch (LJError e) {
+ diagnostics.add(e);
}
- handleStateSetsFromAnnotation(intrface);
- super.visitCtInterface(intrface);
}
@Override
public void visitCtConstructor(CtConstructor c) {
- if (errorEmitter.foundError())
- return;
-
context.enterContext();
- try {
- getRefinementFromAnnotation(c);
- mfc.getConstructorRefinements(c);
- } catch (ParsingException e) {
- return;
- }
+ getRefinementFromAnnotation(c);
+ mfc.getConstructorRefinements(c);
super.visitCtConstructor(c);
context.exitContext();
}
public void visitCtMethod(CtMethod method) {
- if (errorEmitter.foundError())
- return;
-
context.enterContext();
- try {
- mfc.getMethodRefinements(method);
- } catch (ParsingException e) {
- return;
- }
+ mfc.getMethodRefinements(method);
super.visitCtMethod(method);
context.exitContext();
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
index 53b65116..d4d6f89e 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -5,14 +5,14 @@
import java.util.List;
import java.util.Optional;
-import liquidjava.diagnostics.ErrorEmitter;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
import liquidjava.processor.context.*;
import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker;
import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
import liquidjava.rj_language.BuiltinFunctionPredicate;
import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.utils.constants.Formats;
import liquidjava.utils.constants.Keys;
import liquidjava.utils.constants.Types;
@@ -47,16 +47,16 @@
public class RefinementTypeChecker extends TypeChecker {
// This class should do the following:
-
// 1. Keep track of the context variable types
// 2. Do type checking and inference
// Auxiliary TypeCheckers
OperationsChecker otc;
MethodsFunctionsChecker mfc;
+ Diagnostics diagnostics = Diagnostics.getInstance();
- public RefinementTypeChecker(Context context, Factory factory, ErrorEmitter errorEmitter) {
- super(context, factory, errorEmitter);
+ public RefinementTypeChecker(Context context, Factory factory) {
+ super(context, factory);
otc = new OperationsChecker(this);
mfc = new MethodsFunctionsChecker(this);
}
@@ -65,78 +65,69 @@ public RefinementTypeChecker(Context context, Factory factory, ErrorEmitter erro
@Override
public void visitCtClass(CtClass ctClass) {
- if (errorEmitter.foundError()) {
- return;
- }
-
// System.out.println("CTCLASS:"+ctClass.getSimpleName());
context.reinitializeContext();
- super.visitCtClass(ctClass);
+
+ try {
+ super.visitCtClass(ctClass);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
+
}
@Override
public void visitCtInterface(CtInterface intrface) {
- if (errorEmitter.foundError()) {
- return;
- }
-
// System.out.println("CT INTERFACE: " +intrface.getSimpleName());
if (getExternalRefinement(intrface).isPresent()) {
return;
}
- super.visitCtInterface(intrface);
+ try {
+ super.visitCtInterface(intrface);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
}
@Override
public void visitCtAnnotationType(CtAnnotationType annotationType) {
- if (errorEmitter.foundError()) {
- return;
- }
super.visitCtAnnotationType(annotationType);
}
@Override
public void visitCtConstructor(CtConstructor c) {
- if (errorEmitter.foundError()) {
- return;
- }
-
context.enterContext();
mfc.loadFunctionInfo(c);
- super.visitCtConstructor(c);
+ try {
+ super.visitCtConstructor(c);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
context.exitContext();
}
public void visitCtMethod(CtMethod method) {
- if (errorEmitter.foundError()) {
- return;
- }
-
context.enterContext();
if (!method.getSignature().equals("main(java.lang.String[])")) {
mfc.loadFunctionInfo(method);
}
- super.visitCtMethod(method);
+ try {
+ super.visitCtMethod(method);
+ } catch (LJError e) {
+ diagnostics.add(e);
+ }
context.exitContext();
}
@Override
public void visitCtLocalVariable(CtLocalVariable localVariable) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtLocalVariable(localVariable);
// only declaration, no assignment
if (localVariable.getAssignment() == null) {
- Optional a;
- try {
- a = getRefinementFromAnnotation(localVariable);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
- context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()),
- localVariable);
+ Optional a = getRefinementFromAnnotation(localVariable);
+ RefinedVariable v = context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(),
+ a.orElse(new Predicate()), localVariable);
+ getMessageFromAnnotation(localVariable).ifPresent(v::setMessage);
} else {
String varName = localVariable.getSimpleName();
CtExpression e = localVariable.getAssignment();
@@ -146,34 +137,18 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) {
refinementFound = new Predicate();
}
context.addVarToContext(varName, localVariable.getType(), new Predicate(), e);
-
- try {
- checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable,
- localVariable);
- } catch (ParsingException e1) {
- return; // error already in ErrorEmitter
- }
-
+ checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable);
AuxStateHandler.addStateRefinements(this, varName, e);
}
}
@Override
public void visitCtNewArray(CtNewArray newArray) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtNewArray(newArray);
List> l = newArray.getDimensionExpressions();
// TODO only working for 1 dimension
for (CtExpression exp : l) {
- Predicate c;
- try {
- c = getExpressionRefinements(exp);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ Predicate c = getExpressionRefinements(exp);
String name = String.format(Formats.FRESH, context.getCounter());
if (c.getVariableNames().contains(Keys.WILDCARD)) {
c = c.substituteVariable(Keys.WILDCARD, name);
@@ -182,23 +157,15 @@ public void visitCtNewArray(CtNewArray newArray) {
}
context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp);
Predicate ep;
- try {
- ep = Predicate.createEquals(
- BuiltinFunctionPredicate.builtin_length(Keys.WILDCARD, newArray, getErrorEmitter()),
- Predicate.createVar(name));
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray),
+ Predicate.createVar(name));
+
newArray.putMetadata(Keys.REFINEMENT, ep);
}
}
@Override
public void visitCtThisAccess(CtThisAccess thisAccess) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtThisAccess(thisAccess);
CtClass c = thisAccess.getParent(CtClass.class);
String s = c.getSimpleName();
@@ -211,11 +178,7 @@ public void visitCtThisAccess(CtThisAccess thisAccess) {
@SuppressWarnings("unchecked")
@Override
- public void visitCtAssignment(CtAssignment assignment) {
- if (errorEmitter.foundError()) {
- return;
- }
-
+ public void visitCtAssignment(CtAssignment assignment) throws LJError {
super.visitCtAssignment(assignment);
CtExpression ex = assignment.getAssigned();
@@ -225,8 +188,7 @@ public void visitCtAssignment(CtAssignment assignment) {
String name = var.getSimpleName();
checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl);
- } else if (ex instanceof CtFieldWrite) {
- CtFieldWrite fw = ((CtFieldWrite) ex);
+ } else if (ex instanceof CtFieldWrite fw) {
CtFieldReference cr = fw.getVariable();
CtField f = fw.getVariable().getDeclaration();
String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
@@ -237,19 +199,10 @@ public void visitCtAssignment(CtAssignment assignment) {
AuxStateHandler.updateGhostField(fw, this);
}
}
- // if (ex instanceof CtArrayWrite) {
- // Predicate c = getRefinement(ex);
- // TODO continue
- // c.substituteVariable(WILD_VAR, );
- // }
}
@Override
public void visitCtArrayRead(CtArrayRead arrayRead) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtArrayRead(arrayRead);
String name = String.format(Formats.INSTANCE, "arrayAccess", context.getCounter());
context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead);
@@ -259,10 +212,6 @@ public void visitCtArrayRead(CtArrayRead arrayRead) {
@Override
public void visitCtLiteral(CtLiteral lit) {
- if (errorEmitter.foundError()) {
- return;
- }
-
List types = Arrays.asList(Types.IMPLEMENTED);
String type = lit.getType().getQualifiedName();
if (types.contains(type)) {
@@ -281,26 +230,15 @@ public void visitCtLiteral(CtLiteral lit) {
@Override
public void visitCtField(CtField f) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtField(f);
- Optional c;
- try {
- c = getRefinementFromAnnotation(f);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
- // context.addVarToContext(f.getSimpleName(), f.getType(),
- // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new
- // Predicate()) );
- String nname = String.format(Formats.THIS, f.getSimpleName());
+ Optional c = getRefinementFromAnnotation(f);
+ String name = String.format(Formats.THIS, f.getSimpleName());
Predicate ret = new Predicate();
if (c.isPresent()) {
- ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname);
+ ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
}
- RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f);
+ RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f);
+ getMessageFromAnnotation(f).ifPresent(v::setMessage);
if (v instanceof Variable) {
((Variable) v).setLocation("this");
}
@@ -308,10 +246,6 @@ public void visitCtField(CtField f) {
@Override
public void visitCtFieldRead(CtFieldRead fieldRead) {
- if (errorEmitter.foundError()) {
- return;
- }
-
String fieldName = fieldRead.getVariable().getSimpleName();
if (context.hasVariable(fieldName)) {
RefinedVariable rv = context.getVariableByName(fieldName);
@@ -330,29 +264,21 @@ public void visitCtFieldRead(CtFieldRead fieldRead) {
} else if (fieldRead.getVariable().getSimpleName().equals("length")) {
String targetName = fieldRead.getTarget().toString();
- try {
- fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
- BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter())));
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
+ BuiltinFunctionPredicate.length(targetName, fieldRead)));
+
} else {
fieldRead.putMetadata(Keys.REFINEMENT, new Predicate());
- // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE
+ // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE?
}
-
super.visitCtFieldRead(fieldRead);
}
@Override
public void visitCtVariableRead(CtVariableRead variableRead) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtVariableRead(variableRead);
CtVariable varDecl = variableRead.getVariable().getDeclaration();
- getPutVariableMetadada(variableRead, varDecl.getSimpleName());
+ getPutVariableMetadata(variableRead, varDecl.getSimpleName());
}
/**
@@ -360,65 +286,32 @@ public void visitCtVariableRead(CtVariableRead variableRead) {
*/
@Override
public void visitCtBinaryOperator(CtBinaryOperator operator) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtBinaryOperator(operator);
- try {
- otc.getBinaryOpRefinements(operator);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ otc.getBinaryOpRefinements(operator);
}
@Override
public void visitCtUnaryOperator(CtUnaryOperator operator) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtUnaryOperator(operator);
- try {
- otc.getUnaryOpRefinements(operator);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ otc.getUnaryOpRefinements(operator);
}
public void visitCtInvocation(CtInvocation invocation) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtInvocation(invocation);
mfc.getInvocationRefinements(invocation);
}
@Override
public void visitCtReturn(CtReturn ret) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtReturn(ret);
mfc.getReturnRefinements(ret);
}
@Override
public void visitCtIf(CtIf ifElement) {
- if (errorEmitter.foundError()) {
- return;
- }
-
CtExpression exp = ifElement.getCondition();
+ Predicate expRefs = getExpressionRefinements(exp);
- Predicate expRefs;
- try {
- expRefs = getExpressionRefinements(exp);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
String freshVarName = String.format(Formats.FRESH, context.getCounter());
expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName);
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
@@ -463,28 +356,14 @@ public void visitCtIf(CtIf ifElement) {
@Override
public void visitCtArrayWrite(CtArrayWrite arrayWrite) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtArrayWrite(arrayWrite);
CtExpression index = arrayWrite.getIndexExpression();
- BuiltinFunctionPredicate fp;
- try {
- fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(),
- Keys.WILDCARD, arrayWrite, getErrorEmitter());
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(index.toString(), Keys.WILDCARD, arrayWrite);
arrayWrite.putMetadata(Keys.REFINEMENT, fp);
}
@Override
public void visitCtConditional(CtConditional conditional) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtConditional(conditional);
Predicate cond = getRefinement(conditional.getCondition());
Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()),
@@ -494,28 +373,20 @@ public void visitCtConditional(CtConditional conditional) {
@Override
public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtConstructorCall(ctConstructorCall);
mfc.getConstructorInvocationRefinements(ctConstructorCall);
}
@Override
public void visitCtNewClass(CtNewClass newClass) {
- if (errorEmitter.foundError()) {
- return;
- }
-
super.visitCtNewClass(newClass);
}
// ############################### Inner Visitors
// ##########################################
private void checkAssignment(String name, CtTypeReference type, CtExpression ex, CtExpression assignment,
- CtElement parentElem, CtElement varDecl) {
- getPutVariableMetadada(ex, name);
+ CtElement parentElem, CtElement varDecl) throws LJError {
+ getPutVariableMetadata(ex, name);
Predicate refinementFound = getRefinement(assignment);
if (refinementFound == null) {
@@ -531,14 +402,10 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression<
r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName()));
vcChecker.removePathVariableThatIncludes(name); // AQUI!!
- try {
- checkVariableRefinements(refinementFound, name, type, parentElem, varDecl);
- } catch (ParsingException e) {
- return; // error already in ErrorEmitter
- }
+ checkVariableRefinements(refinementFound, name, type, parentElem, varDecl);
}
- private Predicate getExpressionRefinements(CtExpression element) throws ParsingException {
+ private Predicate getExpressionRefinements(CtExpression element) throws LJError {
if (element instanceof CtVariableRead) {
// CtVariableRead elemVar = (CtVariableRead) element;
return getRefinement(element);
@@ -552,7 +419,7 @@ private Predicate getExpressionRefinements(CtExpression element) throws Parsi
return getRefinement(op);
} else if (element instanceof CtLiteral) {
CtLiteral l = (CtLiteral) element;
- return new Predicate(l.getValue().toString(), l, errorEmitter);
+ return new Predicate(l.getValue().toString(), l);
} else if (element instanceof CtInvocation) {
CtInvocation inv = (CtInvocation) element;
visitCtInvocation(inv);
@@ -578,18 +445,17 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) {
// ##########################################
/**
- * @param
+ * Gets the variable refinement from the context and puts it as metadata in the element
+ *
* @param elem
* @param name
- * Cannot be null
*/
- private void getPutVariableMetadada(CtElement elem, String name) {
+ private void getPutVariableMetadata(CtElement elem, String name) {
Predicate cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(name));
Optional ovi = context.getLastVariableInstance(name);
if (ovi.isPresent()) {
cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(ovi.get().getName()));
}
-
elem.putMetadata(Keys.REFINEMENT, cref);
}
}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
index 375bff40..31c019bc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -1,12 +1,12 @@
package liquidjava.processor.refinement_checker;
import java.lang.annotation.Annotation;
-import java.util.Arrays;
+import java.util.Collections;
import java.util.List;
+import java.util.Map;
import java.util.Optional;
-import liquidjava.diagnostics.ErrorEmitter;
-import liquidjava.diagnostics.ErrorHandler;
+import liquidjava.diagnostics.errors.*;
import liquidjava.processor.context.AliasWrapper;
import liquidjava.processor.context.Context;
import liquidjava.processor.context.GhostFunction;
@@ -15,8 +15,8 @@
import liquidjava.processor.facade.AliasDTO;
import liquidjava.processor.facade.GhostDTO;
import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.ParsingException;
import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.utils.Utils;
import liquidjava.utils.constants.Formats;
import liquidjava.utils.constants.Keys;
import liquidjava.utils.constants.Types;
@@ -32,18 +32,18 @@
import spoon.reflect.reference.CtTypeReference;
import spoon.reflect.visitor.CtScanner;
+import static liquidjava.processor.refinement_checker.TypeCheckingUtils.*;
+
public abstract class TypeChecker extends CtScanner {
- Context context;
- Factory factory;
- VCChecker vcChecker;
- ErrorEmitter errorEmitter;
+ protected final Context context;
+ protected final Factory factory;
+ protected final VCChecker vcChecker;
- public TypeChecker(Context c, Factory fac, ErrorEmitter errorEmitter) {
- this.context = c;
- this.factory = fac;
- this.errorEmitter = errorEmitter;
- vcChecker = new VCChecker(errorEmitter);
+ public TypeChecker(Context context, Factory factory) {
+ this.context = context;
+ this.factory = factory;
+ this.vcChecker = new VCChecker();
}
public Context getContext() {
@@ -59,43 +59,54 @@ public Predicate getRefinement(CtElement elem) {
return c == null ? new Predicate() : c;
}
- public Optional getRefinementFromAnnotation(CtElement element) throws ParsingException {
+ public Optional getRefinementFromAnnotation(CtElement element) throws LJError {
Optional constr = Optional.empty();
Optional ref = Optional.empty();
for (CtAnnotation ann : element.getAnnotations()) {
String an = ann.getActualAnnotation().annotationType().getCanonicalName();
if (an.contentEquals("liquidjava.specification.Refinement")) {
- String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value"));
- // CtLiteral s = (CtLiteral) ann.getAllValues().get("value");
+ String st = getStringFromAnnotation(ann.getValue("value"));
ref = Optional.of(st);
} else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) {
- String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value"));
+ String st = getStringFromAnnotation(ann.getValue("value"));
getGhostFunction(st, element);
} else if (an.contentEquals("liquidjava.specification.RefinementAlias")) {
- String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value"));
+ String st = getStringFromAnnotation(ann.getValue("value"));
handleAlias(st, element);
}
}
if (ref.isPresent()) {
- Predicate p = new Predicate(ref.get(), element, errorEmitter);
+ Predicate p = new Predicate(ref.get(), element);
// check if refinement is valid
if (!p.getExpression().isBooleanExpression()) {
- ErrorHandler.printCustomError(element, "Refinement predicate must be a boolean expression",
- errorEmitter);
+ throw new InvalidRefinementError(element.getPosition(),
+ "Refinement predicate must be a boolean expression", ref.get());
}
- if (errorEmitter.foundError())
- return Optional.empty();
-
constr = Optional.of(p);
}
return constr;
}
+ @SuppressWarnings({ "rawtypes" })
+ public Optional getMessageFromAnnotation(CtElement element) {
+ for (CtAnnotation ann : element.getAnnotations()) {
+ String an = ann.getActualAnnotation().annotationType().getCanonicalName();
+ if (an.contentEquals("liquidjava.specification.Refinement")) {
+ Map values = ann.getAllValues();
+ String msg = getStringFromAnnotation((values.get("msg")));
+ if (msg != null && !msg.isEmpty()) {
+ return Optional.of(msg);
+ }
+ }
+ }
+ return Optional.empty();
+ }
+
@SuppressWarnings("unchecked")
- public void handleStateSetsFromAnnotation(CtElement element) {
+ public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
int set = 0;
for (CtAnnotation ann : element.getAnnotations()) {
String an = ann.getActualAnnotation().annotationType().getCanonicalName();
@@ -105,12 +116,12 @@ public void handleStateSetsFromAnnotation(CtElement element) {
}
if (an.contentEquals("liquidjava.specification.Ghost")) {
CtLiteral s = (CtLiteral) ann.getAllValues().get("value");
- createStateGhost(s.getValue(), ann, an, element);
+ createStateGhost(s.getValue(), ann, element);
}
}
}
- private void createStateSet(CtNewArray e, int set, CtElement element) {
+ private void createStateSet(CtNewArray e, int set, CtElement element) throws LJError {
// if any of the states starts with uppercase, throw error (reserved for alias)
for (CtExpression ce : e.getElements()) {
@@ -119,14 +130,13 @@ private void createStateSet(CtNewArray e, int set, CtElement element) {
CtLiteral s = (CtLiteral