Renamed @usedef() to @reveal()

viperproject · Oct 31, 2023 · afa3f08 · afa3f08
1 parent 7dd8a62
commit afa3f08
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
@@ -773,7 +773,7 @@ object evaluator extends EvaluationRules {
                 case Some(a) if a.values.contains("opaque") =>
                   val funcAppAnn = fapp.info.getUniqueInfo[AnnotationInfo]
                   funcAppAnn match {
-                    case Some(a) if a.values.contains("useDef") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
+                    case Some(a) if a.values.contains("reveal") => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)
                     case _ => App(functionSupporter.limitedVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
                   }
                 case _ => App(v3.symbolConverter.toFunction(func), snap1 :: tArgs)

diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
@@ -133,7 +133,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
           case Some(a) if a.values.contains("opaque") =>
             val funcAppAnn = eFApp.info.getUniqueInfo[AnnotationInfo]
             funcAppAnn match {
-              case Some(a) if a.values.contains("useDef") => symbolConverter.toFunction(silverFunc)
+              case Some(a) if a.values.contains("reveal") => symbolConverter.toFunction(silverFunc)
               case _ => functionSupporter.limitedVersion(symbolConverter.toFunction(silverFunc))
             }
           case _ => symbolConverter.toFunction(silverFunc)