From 607995884279572dd55dd4655f2d14525dded9ed Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Sun, 7 Jan 2024 17:04:09 +0000 Subject: [PATCH] Reformatted code --- .../algorithm/bounded/BoundedChecker.kt | 32 ++++++++++--------- .../patterns/constraints/GraphConstraint.kt | 1 + .../bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 8 ++--- .../cli/checkers/ConfigToBoundedChecker.kt | 9 ++++-- .../xcfa/cli/checkers/ConfigToCegarChecker.kt | 3 +- .../xcfa/cli/checkers/ConfigToPortfolio.kt | 4 +-- .../xcfa/cli/checkers/InProcessChecker.kt | 25 +++++++++------ .../mit/theta/xcfa/cli/params/TypeAdapters.kt | 8 ++--- .../mit/theta/xcfa/cli/params/Validators.kt | 4 +-- .../mit/theta/xcfa/cli/params/XcfaConfig.kt | 9 +++--- .../xcfa/cli/utils/CachingFileSerializer.kt | 3 +- .../mit/theta/xcfa/cli/utils/PropertyUtils.kt | 2 +- .../mit/theta/xcfa/cli/utils/XcfaParser.kt | 2 +- 13 files changed, 63 insertions(+), 47 deletions(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt index 2d6128e3e2..8213b8f0d6 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt @@ -35,7 +35,7 @@ import hu.bme.mit.theta.solver.ItpSolver import hu.bme.mit.theta.solver.Solver import java.util.* -class BoundedChecker( +class BoundedChecker( private val monolithicExpr: MonolithicExpr, private val shouldGiveUp: (Int) -> Boolean = { false }, private val bmcSolver: Solver? = null, @@ -47,22 +47,24 @@ class BoundedChecker( private val valToState: (Valuation) -> S, private val biValToAction: (Valuation, Valuation) -> A, private val logger: Logger, -): SafetyChecker { +) : SafetyChecker { + private val vars = monolithicExpr.vars() private val unfoldedInitExpr = PathUtils.unfold(monolithicExpr.initExpr, 0) - private val unfoldedPropExpr = {i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i)} + private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) } private val indices = mutableListOf(VarIndexingFactory.indexing(0)) private val exprs = mutableListOf>() init { - check(bmcSolver != itpSolver || bmcSolver == null) {"Use distinct solvers for BMC and IMC!"} - check(bmcSolver != indSolver || bmcSolver == null) {"Use distinct solvers for BMC and KInd!"} - check(itpSolver != indSolver || itpSolver == null) {"Use distinct solvers for IMC and KInd!"} + check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" } + check(bmcSolver != indSolver || bmcSolver == null) { "Use distinct solvers for BMC and KInd!" } + check(itpSolver != indSolver || itpSolver == null) { "Use distinct solvers for IMC and KInd!" } } + override fun check(prec: UnitPrec?): SafetyResult { var iteration = 0; - while(!shouldGiveUp(iteration)) { + while (!shouldGiveUp(iteration)) { iteration++ logger.write(Logger.Level.MAINSTEP, "Starting iteration $iteration\n") @@ -70,15 +72,15 @@ class BoundedChecker( indices.add(indices.last().add(monolithicExpr.offsetIndex)) - if(bmcEnabled(iteration)) { + if (bmcEnabled(iteration)) { bmc()?.let { return it } } - if(kindEnabled(iteration)) { + if (kindEnabled(iteration)) { kind()?.let { return it } } - if(imcEnabled(iteration)) { + if (imcEnabled(iteration)) { itp()?.let { return it } } } @@ -94,7 +96,7 @@ class BoundedChecker( bmcSolver.add(exprs) bmcSolver.add(Not(unfoldedPropExpr(indices.last()))) - val ret = if(bmcSolver.check().isSat) { + val ret = if (bmcSolver.check().isSat) { val trace = getTrace(bmcSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n") SafetyResult.unsafe(trace) @@ -113,7 +115,7 @@ class BoundedChecker( indSolver.add(exprs) indSolver.add(Not(unfoldedPropExpr(indices.last()))) - val ret = if(indSolver.check().isUnsat) { + val ret = if (indSolver.check().isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in k-induction step\n") SafetyResult.safe() } else null @@ -141,7 +143,7 @@ class BoundedChecker( val status = itpSolver.check() - if(status.isSat) { + if (status.isSat) { val trace = getTrace(itpSolver.model) logger.write(Logger.Level.MAINSTEP, "CeX found in IMC/BMC step (length ${trace.length()})\n") itpSolver.pop() @@ -150,7 +152,7 @@ class BoundedChecker( } var img = unfoldedInitExpr - while(itpSolver.check().isUnsat) { + while (itpSolver.check().isUnsat) { val interpolant = itpSolver.getInterpolant(pattern) val itpFormula = PathUtils.unfold(PathUtils.foldin(interpolant.eval(a), indices[1]), indices[0]) itpSolver.pop() @@ -159,7 +161,7 @@ class BoundedChecker( itpSolver.add(a, itpFormula) itpSolver.add(a, Not(img)) val itpStatus = itpSolver.check() - if(itpStatus.isUnsat) { + if (itpStatus.isUnsat) { logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n") itpSolver.pop() itpSolver.pop() diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt index e50a4bc967..5184928bda 100644 --- a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt +++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/patterns/constraints/GraphConstraint.kt @@ -19,6 +19,7 @@ package hu.bme.mit.theta.graphsolver.patterns.constraints import hu.bme.mit.theta.graphsolver.compilers.GraphPatternCompiler typealias MCM = Collection + sealed interface GraphConstraint { fun accept(compiler: GraphPatternCompiler): T 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 index f07ed3f526..1b2c2411ba 100644 --- 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 @@ -55,7 +55,7 @@ import java.io.File import java.util.concurrent.TimeUnit import kotlin.random.Random -fun runConfig(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger): SafetyResult<*, *> { +fun runConfig(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): SafetyResult<*, *> { propagateInputOptions(config, logger, uniqueLogger) registerAllSolverManagers(config.backendConfig.solverHome, logger) @@ -74,7 +74,7 @@ fun runConfig(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger): Sa } -private fun propagateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger) { +private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { config.inputConfig.property = determineProperty(config, logger) LbePass.level = config.frontendConfig.lbeLevel if (config.backendConfig.backend == Backend.CEGAR) { @@ -93,7 +93,7 @@ private fun propagateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqu ARGWebDebugger.on = config.debugConfig.argdebug } -private fun validateInputOptions(config: XcfaConfig<*,*>, logger: Logger, uniqueLogger: Logger) { +private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) { rule("NoCoiWhenDataRace") { (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && config.inputConfig.property == ErrorDetection.DATA_RACE @@ -102,7 +102,7 @@ private fun validateInputOptions(config: XcfaConfig<*,*>, logger: Logger, unique } fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Triple { - if(config.inputConfig.xcfaWCtx != null) { + if (config.inputConfig.xcfaWCtx != null) { val xcfa = config.inputConfig.xcfaWCtx!!.first ConeOfInfluence = if (config.inputConfig.xcfaWCtx!!.third.multiThreading) { XcfaCoiMultiThread(xcfa) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt index dca52847cb..1e69b7fa36 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt @@ -53,11 +53,14 @@ fun getBoundedChecker(xcfa: XCFA, mcm: MCM, return BoundedChecker( monolithicExpr = getMonolithicExpr(xcfa), - bmcSolver = getSolver(boundedConfig.bmcConfig.bmcSolver, boundedConfig.bmcConfig.validateBMCSolver).createSolver(), + bmcSolver = getSolver(boundedConfig.bmcConfig.bmcSolver, + boundedConfig.bmcConfig.validateBMCSolver).createSolver(), bmcEnabled = { !boundedConfig.bmcConfig.disable }, - itpSolver = getSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver).createItpSolver(), + itpSolver = getSolver(boundedConfig.itpConfig.itpSolver, + boundedConfig.itpConfig.validateItpSolver).createItpSolver(), imcEnabled = { !boundedConfig.itpConfig.disable }, - indSolver = getSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver).createSolver(), + indSolver = getSolver(boundedConfig.indConfig.indSolver, + boundedConfig.indConfig.validateIndSolver).createSolver(), kindEnabled = { !boundedConfig.indConfig.disable }, valToState = { valToState(xcfa, it) }, biValToAction = { val1, val2 -> valToAction(xcfa, val1, val2) }, diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt index 693a69a8f4..4d0ed6bfff 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt @@ -61,7 +61,8 @@ fun getCegarChecker(xcfa: XCFA, mcm: MCM, } val abstractionSolverInstance = abstractionSolverFactory.createSolver() - val globalStatePartialOrd: PartialOrd = cegarConfig.abstractorConfig.domain.partialOrd(abstractionSolverInstance) + val globalStatePartialOrd: PartialOrd = cegarConfig.abstractorConfig.domain.partialOrd( + abstractionSolverInstance) val corePartialOrd: PartialOrd> = if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd) else getStackPartialOrder(globalStatePartialOrd) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt index 12ed4554cd..3114f4e733 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt @@ -46,13 +46,13 @@ fun getPortfolioChecker(xcfa: XCFA, mcm: MCM, config: XcfaConfig<*, *>, val sw = Stopwatch.createStarted() val portfolioName = (config.backendConfig.specConfig as PortfolioConfig).portfolio - val portfolioStm = when(portfolioName) { + val portfolioStm = when (portfolioName) { "COMPLEX", "COMPLEX24" -> complexPortfolio24(xcfa, mcm, parseContext, config, logger, uniqueLogger) "COMPLEX23" -> complexPortfolio23(xcfa, mcm, parseContext, config, logger, uniqueLogger) else -> { - if(File(portfolioName).exists()) { + if (File(portfolioName).exists()) { val kotlinEngine: ScriptEngine = ScriptEngineManager().getEngineByExtension("kts") val bindings: Bindings = SimpleBindings() bindings["xcfa"] = xcfa diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt index 5dbbd7c560..2b49bd964c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/InProcessChecker.kt @@ -40,7 +40,7 @@ import java.util.* import java.util.concurrent.TimeUnit import kotlin.io.path.createTempDirectory -class InProcessChecker( +class InProcessChecker( val xcfa: XCFA, val config: XcfaConfig, val parseContext: ParseContext, @@ -55,7 +55,9 @@ class InProcessChecker( val tempDir = createTempDirectory(config.outputConfig.resultFolder.toPath()) val xcfaJson = CachingFileSerializer.serialize("xcfa.json", xcfa) { getGson(xcfa).toJson(xcfa) } - val parseContextJson = CachingFileSerializer.serialize("parseContext.json", parseContext) { getGson(xcfa).toJson(parseContext) } + val parseContextJson = CachingFileSerializer.serialize("parseContext.json", parseContext) { + getGson(xcfa).toJson(parseContext) + } val processConfig = config.copy( inputConfig = config.inputConfig.copy( @@ -74,7 +76,9 @@ class InProcessChecker( ) ) - val configJson = CachingFileSerializer.serialize("config.json", processConfig) { getGson(xcfa).toJson(processConfig) } + val configJson = CachingFileSerializer.serialize("config.json", processConfig) { + getGson(xcfa).toJson(processConfig) + } val pb = NuProcessBuilder(listOf( ProcessHandle.current().info().command().orElse("java"), @@ -98,7 +102,8 @@ class InProcessChecker( process.destroy(true) throw ErrorCodeException(ExitCodes.TIMEOUT.code) } else { - logger.write(Logger.Level.RESULT,"Config timed out but started writing result, trying to wait an additional 10%...") + logger.write(Logger.Level.RESULT, + "Config timed out but started writing result, trying to wait an additional 10%...") val retCode = process.waitFor(config.backendConfig.timeoutMs / 10, TimeUnit.MILLISECONDS) if (retCode != 0) { throw ErrorCodeException(retCode) @@ -120,24 +125,26 @@ class InProcessChecker( return booleanSafetyResult as SafetyResult, XcfaAction> } - private class ProcessHandler: NuAbstractProcessHandler() { + private class ProcessHandler : NuAbstractProcessHandler() { + private val stdout = LinkedList() private var stdoutRemainder = "" private val stderr = LinkedList() private var stderrRemainder = "" var safetyResult: SafetyResult<*, *>? = null private set + override fun onStdout(buffer: ByteBuffer, closed: Boolean) { - if(!closed) { + if (!closed) { val bytes = ByteArray(buffer.remaining()) buffer[bytes] val str = bytes.decodeToString() stdoutRemainder += str - if(stdoutRemainder.contains("SafetyResult Safe")) { + if (stdoutRemainder.contains("SafetyResult Safe")) { safetyResult = SafetyResult.safe() } - if(stdoutRemainder.contains("SafetyResult Unsafe")) { + if (stdoutRemainder.contains("SafetyResult Unsafe")) { safetyResult = SafetyResult.unsafe() } @@ -151,7 +158,7 @@ class InProcessChecker( } override fun onStderr(buffer: ByteBuffer, closed: Boolean) { - if(!closed) { + if (!closed) { val bytes = ByteArray(buffer.remaining()) buffer[bytes] val str = bytes.decodeToString() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/TypeAdapters.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/TypeAdapters.kt index 90c0c4137a..d0ef7f9bdd 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/TypeAdapters.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/TypeAdapters.kt @@ -23,7 +23,7 @@ import com.google.gson.stream.JsonToken import com.google.gson.stream.JsonWriter import hu.bme.mit.theta.xcfa.passes.LbePass -class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter>() { +class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson) : TypeAdapter>() { private lateinit var gson: Gson @@ -35,7 +35,7 @@ class SpecFrontendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapter Gson): TypeAdapter Gson): TypeAdapter>() { +class SpecBackendConfigTypeAdapter(val gsonSupplier: () -> Gson) : TypeAdapter>() { private lateinit var gson: Gson @@ -105,7 +105,7 @@ class SpecBackendConfigTypeAdapter(val gsonSupplier: () -> Gson): TypeAdapterBoolean) { - if(test()) { +fun rule(name: String, test: () -> Boolean) { + if (test()) { throw ParameterException("Validation failed for rule $name") } } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt index 9d2366e77a..1848907594 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt @@ -45,7 +45,7 @@ interface SpecializableConfig : Config { override fun update(): Boolean = specConfig?.update() ?: createSpecConfig().let { specConfig != null } } -data class XcfaConfig( +data class XcfaConfig( val inputConfig: InputConfig = InputConfig(), val frontendConfig: FrontendConfig = FrontendConfig(), val backendConfig: BackendConfig = BackendConfig(), @@ -77,7 +77,8 @@ data class InputConfig( description = "XCFA and ParseContext (will overwrite --input and --parse-ctx when given)") var xcfaWCtx: Triple? = null, - @Parameter(names = ["--property-file"], description = "Path of the property file (will overwrite --property when given)") + @Parameter(names = ["--property-file"], + description = "Path of the property file (will overwrite --property when given)") var propertyFile: File? = null, @Parameter(names = ["--property"], description = "Property") @@ -85,7 +86,7 @@ data class InputConfig( ) : Config interface SpecFrontendConfig : Config -data class FrontendConfig( +data class FrontendConfig( @Parameter(names = ["--lbe"], description = "Level of LBE (NO_LBE, LBE_LOCAL, LBE_SEQ, LBE_FULL)") var lbeLevel: LbePass.LbeLevel = LbePass.LbeLevel.LBE_SEQ, @@ -122,7 +123,7 @@ data class CHCFrontendConfig( interface SpecBackendConfig : Config -data class BackendConfig( +data class BackendConfig( @Parameter(names = ["--backend"], description = "Backend analysis to use") var backend: Backend = Backend.CEGAR, diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/CachingFileSerializer.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/CachingFileSerializer.kt index a814a8de53..d5327e3a32 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/CachingFileSerializer.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/CachingFileSerializer.kt @@ -19,6 +19,7 @@ package hu.bme.mit.theta.xcfa.cli.utils import java.io.File object CachingFileSerializer { + private val cache: MutableMap, File> = LinkedHashMap() /** @@ -27,7 +28,7 @@ object CachingFileSerializer { * func: generator function if a cache miss occurs */ fun serialize(key: String, obj: Any, func: (Any) -> String): File = - if(cache.containsKey(Pair(key, obj))) { + if (cache.containsKey(Pair(key, obj))) { cache[Pair(key, obj)]!! } else { val str = func(obj) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt index c3e36ea023..ce274d5692 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/PropertyUtils.kt @@ -20,7 +20,7 @@ import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.xcfa.analysis.ErrorDetection import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig -fun determineProperty(config: XcfaConfig<*,*>, logger: Logger): ErrorDetection = config.inputConfig.propertyFile?.run { +fun determineProperty(config: XcfaConfig<*, *>, logger: Logger): ErrorDetection = config.inputConfig.propertyFile?.run { val propertyFile = config.inputConfig.propertyFile!! when { propertyFile.name.endsWith("unreach-call.prp") -> { diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt index 8b58795753..965af5fd30 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaParser.kt @@ -41,7 +41,7 @@ import javax.script.ScriptEngineManager import kotlin.system.exitProcess -fun getXcfa(config: XcfaConfig<*,*>, parseContext: ParseContext, logger: Logger, uniqueWarningLogger: Logger) = +fun getXcfa(config: XcfaConfig<*, *>, parseContext: ParseContext, logger: Logger, uniqueWarningLogger: Logger) = try { when (config.frontendConfig.inputType) { InputType.CHC -> {