Set this As Default Argument in Ghost Invocations

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/input_reader_correct/Test.java

@@ -1,16 +1,12 @@
 package testSuite.classes.input_reader_correct;
 
-@SuppressWarnings("unused")
+import java.io.InputStreamReader;
+
 public class Test {
     public static void main(String[] args) throws Exception {
-        // Arrays are not well supported in LiquidJava
-
-        // InputStreamReader isr = new InputStreamReader(new FileInputStream("test1.txt"));
-        // @Refinement("_ > -9")
-        // int a = isr.read();
-        // char[] arr = new char[20];
-        // int b = isr.read(arr, 10, 5);
-        // System.out.println(arr);
-        // isr.close();
+        InputStreamReader is = new InputStreamReader(System.in);
+        is.read();
+        is.read();
+        is.close();
     }
 }

liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/InputStreamReaderRefs.java

@@ -0,0 +1,31 @@
+package testSuite.classes.input_reader_correct_default_this;
+
+import java.io.InputStream;
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+// https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
+@ExternalRefinementsFor("java.io.InputStreamReader")
+public interface InputStreamReaderRefs {
+
+    @RefinementPredicate("boolean open(InputStreamReader i)")
+    @StateRefinement(to = "open()")
+    public void InputStreamReader(InputStream in);
+
+    @StateRefinement(from = "open()", to = "open()")
+    @Refinement("(_ >= -1) && (_ <= 127)")
+    public int read();
+
+    @StateRefinement(from = "open()", to = "!open()")
+    public void close();
+
+    @StateRefinement(from = "open()", to = "open()")
+    @Refinement("_ >= -1")
+    public int read(
+            @Refinement("length(cbuf) > 0") char[] cbuf,
+            @Refinement("_ >= 0") int offset,
+            @Refinement("(_ >= 0) && (_ + offset) <= length(cbuf)") int length);
+}

liquidjava-example/src/main/java/testSuite/classes/input_reader_correct_default_this/Test.java

@@ -0,0 +1,12 @@
+package testSuite.classes.input_reader_correct_default_this;
+
+import java.io.InputStreamReader;
+
+public class Test {
+    public static void main(String[] args) throws Exception {
+        InputStreamReader is = new InputStreamReader(System.in);
+        is.read();
+        is.read();
+        is.close();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/input_reader_error/Test.java

@@ -6,7 +6,6 @@
 public class Test {
 
     public static void main(String[] args) throws IOException {
-        // java.io.InputStreamReader.InputStreamReader
         InputStreamReader is = new InputStreamReader(System.in);
         is.read();
         is.read();

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -261,9 +261,9 @@ public static Predicate createVar(String name) {
         return new Predicate(new Var(name));
     }
 
-    public static Predicate createInvocation(String name, Predicate... Predicates) {
+    public static Predicate createInvocation(String name, Predicate... predicates) {
         List<Expression> le = new ArrayList<>();
-        for (Predicate c : Predicates)
+        for (Predicate c : predicates)
             le.add(c.getExpression());
         return new Predicate(new FunctionInvocation(name, le));
     }

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java

@@ -161,9 +161,13 @@ else if (rc instanceof VarContext) {
     private Expression functionCallCreate(FunctionCallContext rc) {
         if (rc.ghostCall() != null) {
             GhostCallContext gc = rc.ghostCall();
-            List<Expression> le = getArgs(gc.args());
             String name = Utils.qualifyName(prefix, gc.ID().getText());
-            return new FunctionInvocation(name, le);
+            List<Expression> args = getArgs(gc.args());
+            if (args.isEmpty()) {
+                // if no args provided, add "this" as default
+                args.add(new Var("this"));
+            }
+            return new FunctionInvocation(name, args);
         } else {
             AliasCallContext gc = rc.aliasCall();
             List<Expression> le = getArgs(gc.args());