Bugfix

ftsrg · Apr 28, 2024 · cec184e · cec184e
1 parent bc8b847
commit cec184e
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 4 deletions.
diff --git a/.../main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/.../main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java
@@ -161,6 +161,7 @@ public CStatement visitCompilationUnit(CParser.CompilationUnitContext ctx) {
         functions.clear();
 
         // ExpressionVisitor.setBitwise(ctx.accept(BitwiseChecker.instance));
+        ctx.accept(typedefVisitor);
 
         List<CParser.ExternalDeclarationContext> globalUsages = globalDeclUsageVisitor.getGlobalUsages(ctx);
 

diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt
@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.analysis
 import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.core.decl.Decl
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.model.ImmutableValuation
@@ -42,13 +43,21 @@ internal fun <S : ExprState> XcfaState<S>.withGeneralizedVars(): S {
     val varLookup = processes.mapNotNull { (_, process) -> process.varLookup.peek()?.reverseMapping() }
         .reduceOrNull(Map<VarDecl<*>, VarDecl<*>>::plus) ?: mapOf()
     return if (sGlobal.isBottom) sGlobal
-    else when (sGlobal) {
-        is ExplState -> ExplState.of(sGlobal.getVal().changeVars(varLookup))
-        is PredState -> PredState.of(sGlobal.preds.map { p -> p.changeVars(varLookup) })
+    else sGlobal.getState(varLookup)
+}
+
+private fun <S : ExprState> S.getState(varLookup: Map<VarDecl<*>, VarDecl<*>>): S =
+    when (this) {
+        is ExplState -> ExplState.of(getVal().changeVars(varLookup))
+        is PredState -> PredState.of(preds.map { p -> p.changeVars(varLookup) })
+        is PtrState<*> -> PtrState(innerState.getState(varLookup), lastWrites.map {
+            Pair(it.key, it.value.map {
+                Triple(it.first.changeVars(varLookup), it.second.changeVars(varLookup), it.third.changeVars(varLookup))
+            })
+        }.toMap(), nextCnt)
         else -> throw NotImplementedError(
             "Generalizing variable instances is not implemented for data states that are not explicit or predicate.")
     } as S
-}
 
 class LazyDelegate<T, P : Any>(val getProperty: T.() -> P) {