[refactor] translate \fresh in JMLTranslator

Conflicts:
	system/src/de/uka/ilkd/key/speclang/jml/translation/JMLTranslator.java
	system/src/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g

Author: danielgrahl

system/src/de/uka/ilkd/key/speclang/jml/translation/JMLTranslator.java

@@ -24,6 +24,7 @@
 import de.uka.ilkd.key.collection.ImmutableSLList;
 import de.uka.ilkd.key.java.Label;
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.java.TypeConverter;
 import de.uka.ilkd.key.java.abstraction.ArrayType;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.abstraction.PrimitiveType;
@@ -73,7 +74,8 @@ public static enum JMLKeyWord {
         INV_FOR ("\\invariant_for"),
         CAST ("cast"),
         CONDITIONAL ("conditional"),
-        
+        FRESH ("\\fresh"),
+
         // clauses
         ACCESSIBLE ("accessible"),
         ASSIGNABLE ("assignable"),
@@ -824,6 +826,51 @@ public Object translate(SLTranslationExceptionManager excManager,
             }
         });
 
+        translationMethods.put(JMLKeyWord.FRESH,
+                               new JMLTranslationMethod() {
+
+            @Override
+            public SLExpression translate(
+                    SLTranslationExceptionManager excManager,
+                    Object... params)
+                    throws SLTranslationException {
+                checkParameters(params,
+                                ImmutableList.class, 
+                                Services.class);
+                final ImmutableList<SLExpression> list = (ImmutableList) params[0];
+                final Map<LocationVariable,Term> atPres = (Map) params[1];
+                final Services services = (Services) params[2];
+
+	        if(atPres == null || atPres.get(TB.getBaseHeap(services)) == null) {
+	            throw excManager.createException("\\fresh not allowed in this context");
+	        }
+
+	        Term t = TB.tt();
+	        final Sort objectSort = services.getJavaInfo().objectSort();
+                final TypeConverter tc = services.getTypeConverter();
+	        for(SLExpression expr: list) {
+    	            if(!expr.isTerm()) {
+	                throw excManager.createException("Expected a term, but found: " + expr);
+	            } else if(expr.getTerm().sort().extendsTrans(objectSort)) {
+	                t = TB.and(t,
+	                           TB.equals(TB.select(services,
+	                                           tc.getBooleanLDT().targetSort(),
+	                                           atPres.get(TB.getBaseHeap(services)),
+	                                           expr.getTerm(),
+	                                           TB.func(tc.getHeapLDT().getCreated())),
+	                                 TB.FALSE(services)));
+    	            } else if(expr.getTerm().sort().extendsTrans(tc.getLocSetLDT().targetSort())) {
+	            t = TB.and(t, TB.subset(services,
+	                                    expr.getTerm(),
+	                                    TB.freshLocs(services, atPres.get(TB.getBaseHeap(services)))));
+	            } else {
+	                throw excManager.createException("Wrong type: " + expr);
+	            }
+	        }
+	        return new SLExpression(t);
+            }
+        });
+
         // operators
         translationMethods.put(JMLKeyWord.EQUIVALENCE,
                                new JMLEqualityTranslationMethod() {

system/src/de/uka/ilkd/key/speclang/jml/translation/jmlparser.g

@@ -1525,32 +1525,8 @@ jmlprimary returns [SLExpression result=null] throws SLTranslationException
 
     |   FRESH LPAREN list=expressionlist RPAREN
 	{
-	    if(atPres == null || atPres.get(getBaseHeap()) == null) {
-	        raiseError("\\fresh not allowed in this context");
-	    }
-	    t = TB.tt();
-	    final Sort objectSort = services.getJavaInfo().objectSort();
-	    for(SLExpression expr: list) {
-	        if(!expr.isTerm()) {
-	            raiseError("Expected a term, but found: " + expr);
-	        } else if(expr.getTerm().sort().extendsTrans(objectSort)) {
-	            t = TB.and(t, 
-	                       TB.equals(TB.select(services,
-	                                           booleanLDT.targetSort(),
-	                                           atPres.get(getBaseHeap()),
-	                                           expr.getTerm(),
-	                                           TB.func(heapLDT.getCreated())),
-	                                 TB.FALSE(services)));
-	        } else if(expr.getTerm().sort().extendsTrans(locSetLDT.targetSort())) {
-	            t = TB.and(t, TB.subset(services, 
-	                                    expr.getTerm(), 
-	                                    TB.freshLocs(services, atPres.get(getBaseHeap()))));
-	        } else {
-	            raiseError("Wrong type: " + expr);
-	        }
-	    }
-	    result = new SLExpression(t);
-	} 
+        result = translator.translate("\\fresh", SLExpression.class, list, atPres, services);
+	}
 
     |   REACH LPAREN t=storeref COMMA e1=expression COMMA e2=expression (COMMA e3=expression)? RPAREN
 	{