Added more tests

ftsrg · Jul 17, 2024 · 242d55e · 242d55e
1 parent e79bd00
commit 242d55e
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 0 deletions.
diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt
@@ -17,19 +17,23 @@
 package hu.bme.mit.theta.analysis.algorithm
 
 import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker
+import hu.bme.mit.theta.common.OsHelper
 import hu.bme.mit.theta.common.logging.NullLogger
 import hu.bme.mit.theta.core.Relation
 import hu.bme.mit.theta.core.decl.Decls.Param
 import hu.bme.mit.theta.core.plus
 import hu.bme.mit.theta.core.type.inttype.IntExprs.*
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory
 import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Assumptions
 import org.junit.jupiter.api.Test
 
 class HornTest {
 
     @Test
     fun testHornUnsafe() {
+        Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX));
+
         val inv = Relation("inv", Int())
         val p0 = Param("P0", Int())
         val p1 = Param("P1", Int())
@@ -43,6 +47,8 @@ class HornTest {
 
     @Test
     fun testHornSafe() {
+        Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX));
+
         val inv = Relation("inv", Int())
         val p0 = Param("P0", Int())
         val p1 = Param("P1", Int())

diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
@@ -15,9 +15,11 @@
  */
 package hu.bme.mit.theta.xcfa.cli
 
+import hu.bme.mit.theta.common.OsHelper
 import hu.bme.mit.theta.frontend.chc.ChcFrontend
 import hu.bme.mit.theta.xcfa.cli.XcfaCli.Companion.main
 import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Assumptions
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.Arguments
@@ -87,6 +89,19 @@ class XcfaCliVerifyTest {
             )
         }
 
+        @JvmStatic
+        fun cFilesShortInt(): Stream<Arguments> {
+            return Stream.of(
+                Arguments.of("/c/litmustest/singlethread/00assignment.c", null),
+                Arguments.of("/c/litmustest/singlethread/01cast.c", null),
+                Arguments.of("/c/litmustest/singlethread/02types.c", null),
+                Arguments.of("/c/litmustest/singlethread/15addition.c", null),
+                Arguments.of("/c/litmustest/singlethread/20testinline.c", null),
+                Arguments.of("/c/litmustest/singlethread/21namecollision.c", null),
+                Arguments.of("/c/litmustest/singlethread/22nondet.c", null),
+            )
+        }
+
         @JvmStatic
         fun chcFiles(): Stream<Arguments> {
             return Stream.of(
@@ -239,4 +254,19 @@ class XcfaCliVerifyTest {
         main(params)
     }
 
+    @ParameterizedTest
+    @MethodSource("cFilesShortInt")
+    fun testCVerifyCHC(filePath: String, extraArgs: String?) {
+        Assumptions.assumeTrue(OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX));
+
+        val params = arrayOf(
+            "--backend", "CHC",
+            "--input-type", "C",
+            "--input", javaClass.getResource(filePath)!!.path,
+            "--stacktrace",
+            "--debug"
+        )
+        main(params)
+    }
+
 }