Fixed missing arg

ftsrg · Feb 12, 2024 · 9651f98 · 9651f98
1 parent f3bc669
commit 9651f98
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 2 deletions.
diff --git a/...jects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java b/...jects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SafetyResult.java
@@ -157,6 +157,10 @@ private Unsafe() {
             this.cex = Optional.empty();
         }
 
+        public boolean hasTrace() {
+            return cex.isPresent();
+        }
+
         public Trace<S, A> getTrace() {
             return cex.orElseThrow();
         }

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -228,7 +228,7 @@ private fun postVerificationLogging(safetyResult: SafetyResult<*, *>, mcm: MCM,
         logger.write(Logger.Level.INFO,
             "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n")
 
-        if (!config.outputConfig.argConfig.disable && safetyResult.arg != null) {
+        if (!config.outputConfig.argConfig.disable && safetyResult.hasArg()) {
             val argFile = File(resultFolder, "arg-${safetyResult.isSafe}.dot")
             val g: Graph = ArgVisualizer.getDefault().visualize(safetyResult.arg)
             argFile.writeText(GraphvizWriter.getInstance().writeString(g))

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaWitnessWriter.kt
@@ -42,7 +42,7 @@ class XcfaWitnessWriter {
         parseContext: ParseContext,
         witnessfile: File,
     ) {
-        if (safetyResult.isUnsafe && safetyResult.asUnsafe().trace != null) {
+        if (safetyResult.isUnsafe && safetyResult.asUnsafe().hasTrace()) {
             val concrTrace: Trace<XcfaState<ExplState>, XcfaAction> = XcfaTraceConcretizer.concretize(
                 safetyResult.asUnsafe().trace as Trace<XcfaState<*>, XcfaAction>?, cexSolverFactory)