Merge pull request #607 from utwente-fmt/standardize-function-to-pred…

…icate Standardize "resource functions" to predicates
utwente-fmt · Mar 19, 2021 · 682855b · 682855b
2 parents e913e51 + d7088ce
commit 682855b
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 4 deletions.
diff --git a/examples/basic/predicate.pvl b/examples/basic/predicate.pvl
@@ -0,0 +1,7 @@
+//:: case OnlyPredicate
+//:: verdict Pass
+//:: tools silicon carbon
+
+class Pred {
+    resource f() = true;
+}
diff --git a/src/main/java/vct/col/features/FeatureRainbow.scala b/src/main/java/vct/col/features/FeatureRainbow.scala
@@ -170,10 +170,16 @@ class RainbowVisitor(source: ProgramUnit) extends RecursiveVisitor(source, true)
       }
     }
 
-    if(isPure(m) && isInline(m))
-      addFeature(InlinePredicate, m)
-    if(isPure(m) && m.getBody.isInstanceOf[BlockStatement])
-      addFeature(PureImperativeMethods, m)
+    if(isPure(m)) {
+      if(isInline(m))
+        addFeature(InlinePredicate, m)
+      if(m.getBody.isInstanceOf[BlockStatement])
+        addFeature(PureImperativeMethods, m)
+    }
+
+    if(m.kind == Method.Kind.Pure && m.getReturnType.isPrimitive(PrimitiveSort.Resource))
+      addFeature(NotStandardized, m)
+
     if(m.kind == Method.Kind.Constructor)
       addFeature(Constructors, m)
     if(!m.getReturnType.isPrimitive(PrimitiveSort.Void) && !isPure(m))