state changes in the constructor do not add old mentions since when the constructor is called there isnt a old version of the object

Author: CatarinaGamboa

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

@@ -18,7 +18,7 @@ public static void main(String[] args) {
         // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project";
         String file = args.length == 0 ? allPath : args[0];
         ErrorEmitter ee = launch(file);
-        System.out.println(ee.foundError()? (ee.getFullMessage()):("Correct! Passed Verification."));
+        System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification."));
 
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -135,7 +135,7 @@ private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariabl
         if (firstSi != null && lastSi != null) {
             cSMT = firstSi.clone();
             lastSi.setNext(new VCImplication(expectedType));
-             printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType);
+            // printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType); //DEBUG: UNCOMMENT
         }
 
         return cSMT; // firstSi != null ? firstSi : new VCImplication(new Predicate());

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -48,7 +48,6 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
         }
     }
 
-
     /**
      * Creates the list of states and adds them to the function
      *
@@ -67,7 +66,7 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
             Map<String, CtExpression> m = an.getAllValues();
             String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
             ObjectState state = new ObjectState();
-            if (to != null) 
+            if (to != null)
                 state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
             l.add(state);
         }
@@ -80,7 +79,7 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
 
         Predicate[] s = { Predicate.createVar(tc.THIS) };
         Predicate c = new Predicate();
-        List<GhostFunction> sets = getDifferentSets(tc, klass);//??
+        List<GhostFunction> sets = getDifferentSets(tc, klass);// ??
         for (GhostFunction sg : sets) {
             if (sg.getReturnType().toString().equals("int")) {
                 Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
@@ -179,10 +178,6 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
         return state;
     }
 
-
-
-
-
     private static Predicate createStatePredicate(String value, /* RefinedFunction f */
             String targetClass, TypeChecker tc, CtElement e, boolean isTo) throws ParsingException {
         Predicate p = new Predicate(value, e, tc.getErrorEmitter());
@@ -448,7 +443,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
                 for (String s : map.keySet()) {
                     transitionedState = transitionedState.substituteVariable(s, map.get(s));
                 }
-                transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc);      
+                transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc);
                 // update of stata of new instance of this#n#(whatever it was + 1)
                 addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation);
                 return transitionedState;
@@ -466,19 +461,20 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
         return new Predicate();
     }
 
-
     /**
      * Method prepared to change all old vars in a predicate, however it has not been needed yet
+     * 
      * @param pred
      * @param tc
+     * 
      * @return
      */
     private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) {
         Predicate noOld = pred;
         List<String> listVarsInOld = pred.getOldVariableNames();
-        for (String varInOld : listVarsInOld){
+        for (String varInOld : listVarsInOld) {
             Optional<VariableInstance> ovi = tc.getContext().getLastVariableInstance(varInOld);
-            if(ovi.isPresent())
+            if (ovi.isPresent())
                 noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter());
         }
         return noOld;

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

@@ -137,31 +137,29 @@ public Predicate changeOldMentions(String previousName, String newName, ErrorEmi
         return new Predicate(e);
     }
 
-
-    public List<String> getOldVariableNames(){
+    public List<String> getOldVariableNames() {
         List<String> ls = new ArrayList<>();
         expressionGetOldVariableNames(this.exp, ls);
         return ls;
     }
 
-    private void expressionGetOldVariableNames(Expression exp, List<String> ls){
-        if(exp instanceof FunctionInvocation){
+    private void expressionGetOldVariableNames(Expression exp, List<String> ls) {
+        if (exp instanceof FunctionInvocation) {
             FunctionInvocation fi = (FunctionInvocation) exp;
-           if (fi.getName().equals(Utils.OLD)){
+            if (fi.getName().equals(Utils.OLD)) {
                 List<Expression> le = fi.getArgs();
-                for(Expression e: le){
-                    if (e instanceof Var) 
-                       ls.add(((Var) e).getName());
+                for (Expression e : le) {
+                    if (e instanceof Var)
+                        ls.add(((Var) e).getName());
                 }
-           }
-        } 
-        if(exp.hasChildren()){
+            }
+        }
+        if (exp.hasChildren()) {
             for (var ch : exp.getChildren())
                 expressionGetOldVariableNames(ch, ls);
-            
+
         }
     }
-    
 
     public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[] toChange, ErrorEmitter ee) {
         Map<String, Expression> nameRefinementMap = new HashMap<>();