From afa3f0886426b29d5ab5b70efab1b70cc06e3083 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Tue, 31 Oct 2023 13:27:24 +0100 Subject: [PATCH] Renamed @useDef() to @reveal() --- src/main/scala/rules/Evaluator.scala | 2 +- .../functions/HeapAccessReplacingExpressionTranslator.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 43b46e5d3..1797162c0 100644 --- 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 index 8258879ea..5235f31de 100644 --- 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)