fixes unit tests by making type-check caching specific to the config'…

…s choice of 32 or 64bit ints
viperproject · Jun 30, 2023 · 50f379c · 50f379c
1 parent 52317a4
commit 50f379c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -217,7 +217,7 @@ object Info extends LazyLogging {
   private val typeInfoCache: ConcurrentMap[TypeInfoCacheKey, TypeInfoImpl] = new ConcurrentHashMap()
 
   private def getCacheKey(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, () => Either[Vector[VerifierError], ExternalTypeInfo]], isMainContext: Boolean, config: Config): TypeInfoCacheKey = {
-    // the cache key only depends on config's `typeBounds` and `enableLazyImport`
+    // the cache key only depends on config's `typeBounds`, `int32bit`, and `enableLazyImport`
     val pkgKey = pkg.hashCode().toString
     // the computed key must be deterministic!
     val dependentTypeInfoKey = dependentTypeInfo
@@ -227,6 +227,7 @@ object Info extends LazyLogging {
       .mkString("")
     val isMainContextKey = if (isMainContext) "1" else "0"
     val configKey = config.typeBounds.hashCode().toString ++
+      (if (config.int32bit) "1" else "0") ++
       (if (config.enableLazyImports) "1" else "0")
 
     val key = pkgKey ++

diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala
@@ -55,7 +55,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
       packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)),
       checkConsistency = true,
       cacheParserAndTypeChecker = cacheParserAndTypeChecker,
-      z3Exe = z3Exe
+      z3Exe = z3Exe,
     )
 
   override def runTests(testName: Option[String], args: Args): Status = {
@@ -92,7 +92,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
         val source = FromFileSource(input.file)
         val config = getConfig(source)
         val pkgInfo = config.packageInfoInputMap.keys.head
-        val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(pkgInfo, getConfig(source))(executor), Duration.Inf))
+        val (result, elapsedMilis) = time(() => Await.result(gobraInstance.verify(pkgInfo, config)(executor), Duration.Inf))
 
         info(s"Time required: $elapsedMilis ms")