changes to enable debugging and fixing of constructor issue

Author: CatarinaGamboa

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

@@ -100,7 +100,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
         return smtChecks(premises, et, p);
     }
 
-    private /* Predicate */ VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
+    private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
             List<RefinedVariable> vars, HashMap<String, PlacementInCode> map) {
 
         VCImplication firstSi = null;
@@ -135,7 +135,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
         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);
         }
 
         return cSMT; // firstSi != null ? firstSi : new VCImplication(new Predicate());

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

@@ -3,6 +3,8 @@
 import java.lang.annotation.Annotation;
 import java.util.*;
 import java.util.stream.Collectors;
+
+import liquidjava.errors.ErrorEmitter;
 import liquidjava.errors.ErrorHandler;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.TypeChecker;
@@ -40,19 +42,45 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
                     return;
                 }
             }
-            setFunctionStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c);
+            setConstructorStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c);
         } else {
             setDefaultState(f, tc);
         }
     }
 
+
+    /**
+     * Creates the list of states and adds them to the function
+     *
+     * @param f
+     * @param anns
+     * @param tc
+     * @param element
+     * 
+     * @throws ParsingException
+     */
+    @SuppressWarnings({ "rawtypes" })
+    private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<? extends Annotation>> anns,
+            TypeChecker tc, CtElement element) throws ParsingException {
+        List<ObjectState> l = new ArrayList<>();
+        for (CtAnnotation<? extends Annotation> an : anns) {
+            Map<String, CtExpression> m = an.getAllValues();
+            String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
+            ObjectState state = new ObjectState();
+            if (to != null) 
+                state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
+            l.add(state);
+        }
+        f.setAllStates(l);
+    }
+
     public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
         String[] path = f.getTargetClass().split("\\.");
         String klass = path[path.length - 1];
 
         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),
@@ -151,6 +179,10 @@ 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());
@@ -416,7 +448,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;
@@ -434,6 +466,24 @@ 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){
+            Optional<VariableInstance> ovi = tc.getContext().getLastVariableInstance(varInOld);
+            if(ovi.isPresent())
+                noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter());
+        }
+        return noOld;
+    }
+
     private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName,
             TypeChecker tc) {
         return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter());

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

@@ -137,6 +137,32 @@ public Predicate changeOldMentions(String previousName, String newName, ErrorEmi
         return new Predicate(e);
     }
 
+
+    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){
+            FunctionInvocation fi = (FunctionInvocation) exp;
+           if (fi.getName().equals(Utils.OLD)){
+                List<Expression> le = fi.getArgs();
+                for(Expression e: le){
+                    if (e instanceof Var) 
+                       ls.add(((Var) e).getName());
+                }
+           }
+        } 
+        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<>();
         for (GhostState gs : ghostState)