diff --git a/examples/basic/predicate.pvl b/examples/basic/predicate.pvl new file mode 100644 index 0000000000..1a3858286f --- /dev/null +++ b/examples/basic/predicate.pvl @@ -0,0 +1,7 @@ +//:: case OnlyPredicate +//:: verdict Pass +//:: tools silicon carbon + +class Pred { + resource f() = true; +} \ No newline at end of file diff --git a/src/main/java/vct/col/features/FeatureRainbow.scala b/src/main/java/vct/col/features/FeatureRainbow.scala index 9eb753a1f4..28b25495f1 100644 --- 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))