Fixed problem with parsetest

ftsrg · Nov 13, 2023 · ac0e928 · ac0e928
1 parent 3d1e392
commit ac0e928
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 2 deletions.
diff --git a/.../main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java b/.../main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java
@@ -22,6 +22,7 @@
 import hu.bme.mit.theta.core.type.Type;
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.type.bvtype.BvType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.frontend.ParseContext;
 import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
@@ -54,6 +55,7 @@
 import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType;
 
 import java.util.List;
+import java.util.Map.Entry;
 import java.util.Optional;
 
 import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getCastVisitor;
@@ -154,7 +156,29 @@ private static CComplexType getType(Type type, ParseContext parseContext) {
             return new CArray(null, getType(aType.getElemType(), parseContext), parseContext);
         } else if (type instanceof BoolType) {
             return new CBool(null, parseContext);
-        } else throw new RuntimeException("Not yet implemented for type: " + type);
+        } else if (type instanceof BvType) {
+            for (Entry<String, Integer> entry : parseContext.getArchitecture().standardTypeSizes.entrySet()) {
+                String s = entry.getKey();
+                Integer integer = entry.getValue();
+                if (integer == ((BvType) type).getSize()) {
+                    switch (s) {
+                        case "bool":
+                            return new CBool(null, parseContext);
+                        case "short":
+                            return ((BvType) type).getSigned() ? new CSignedShort(null, parseContext) : new CUnsignedShort(null, parseContext);
+                        case "int":
+                            return ((BvType) type).getSigned() ? new CSignedInt(null, parseContext) : new CUnsignedInt(null, parseContext);
+                        case "long":
+                            return ((BvType) type).getSigned() ? new CSignedLong(null, parseContext) : new CUnsignedLong(null, parseContext);
+                        case "longlong":
+                            return ((BvType) type).getSigned() ? new CSignedLongLong(null, parseContext) : new CUnsignedLongLong(null, parseContext);
+                    }
+                }
+            }
+            throw new RuntimeException("No suitable width found for type: " + type);
+        } else {
+            throw new RuntimeException("Not yet implemented for type: " + type);
+        }
     }
 
 

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliParseTest.kt
@@ -170,7 +170,8 @@ class XcfaCliParseTest {
         main(arrayOf(
             "--input-type", "C",
             "--input", javaClass.getResource(filePath)!!.path,
-            "--parse-only", "--stacktrace"
+            "--parse-only", "--stacktrace",
+            "--debug"
         ))
     }
 
@@ -195,6 +196,7 @@ class XcfaCliParseTest {
             "--input", javaClass.getResource(filePath)!!.path,
             "--parse-only",
             "--stacktrace",
+            "--debug"
         ))
     }
 
@@ -206,6 +208,7 @@ class XcfaCliParseTest {
             "--input", javaClass.getResource(filePath)!!.path,
             "--parse-only",
             "--stacktrace",
+            "--debug"
         ))
     }
 
@@ -217,6 +220,7 @@ class XcfaCliParseTest {
             "--input", javaClass.getResource(filePath)!!.path,
             "--parse-only",
             "--stacktrace",
+            "--debug"
         ))
     }
 
@@ -231,13 +235,15 @@ class XcfaCliParseTest {
             "--stacktrace",
             "--output-results",
             "--output-directory", temp.toAbsolutePath().toString(),
+            "--debug"
         ))
         val xcfaJson = temp.resolve("xcfa.json").toFile()
         main(arrayOf(
             "--input-type", "JSON",
             "--input", xcfaJson.absolutePath.toString(),
             "--parse-only",
             "--stacktrace",
+            "--debug"
         ))
         temp.toFile().deleteRecursively()
     }
@@ -253,13 +259,15 @@ class XcfaCliParseTest {
             "--stacktrace",
             "--output-results",
             "--output-directory", temp.toAbsolutePath().toString(),
+            "--debug"
         ))
         val xcfaC = temp.resolve("xcfa.c").toFile()
         main(arrayOf(
             "--input-type", "C",
             "--input", xcfaC.absolutePath.toString(),
             "--parse-only",
             "--stacktrace",
+            "--debug"
         ))
         temp.toFile().deleteRecursively()
     }