diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java index dbb4f971a5..12105b5f8c 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpFromBvExpr.java @@ -85,7 +85,7 @@ public FpLitExpr eval(Valuation val) { public boolean equals(final Object obj) { if (this == obj) { return true; - } else if (obj.getClass() == this.getClass()) { + } else if (obj != null && obj.getClass() == this.getClass()) { final FpFromBvExpr that = (FpFromBvExpr) obj; return this.getOp().equals(that.getOp()) && fpType.equals(that.fpType) && roundingMode.equals(that.roundingMode); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index b13b3938f1..099c5466e4 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -489,8 +489,9 @@ public Expr visitUnaryExpressionCast(CParser.UnaryExpressionCastContext ctx) parseContext.getMetadata().create(expr, "cType", smallestCommonType); return expr; case "&": - checkState(accept instanceof RefExpr && ((RefExpr) accept).getDecl() instanceof VarDecl, "Referencing non-variable expressions is not allowed!"); - return reference((RefExpr) accept); + final Expr localAccept = accept; + checkState(localAccept instanceof RefExpr && ((RefExpr) localAccept).getDecl() instanceof VarDecl, "Referencing non-variable expressions is not allowed!"); + return reference((RefExpr) localAccept); case "*": type = CComplexType.getType(accept, parseContext); checkState(type instanceof CPointer, "Dereferencing non-pointer expression is not allowed!"); diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 839a0ec722..51ea43a5cf 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -59,7 +59,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo if (name == null) return getAnonymousLoc(builder, metadata = metadata) locationLut.putIfAbsent(name, XcfaLocation(name, metadata = metadata)) val location = locationLut[name] - builder.addLoc(location!!) + builder.addLoc(checkNotNull(location)) return location } @@ -199,7 +199,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo memoryMaps[type] = toAdd parseContext.metadata.create(toAdd, "defaultElement", CComplexType.getType(op, parseContext).nullValue) } - val memoryMap = memoryMaps[type]!! + val memoryMap = checkNotNull(memoryMaps[type]) parseContext.metadata.create(op, "dereferenced", true) parseContext.metadata.create(op, "refSubstitute", memoryMap) val write = ArrayExprs.Write(cast(memoryMap.ref, ArrayType.of(ptrType, type)), @@ -690,7 +690,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo } if (cStatement is CCase) { val afterGuard = buildPostStatement(testValue, - ParamPack(builder, endInit!!, breakLoc, continueLoc, returnLoc)) + ParamPack(builder, checkNotNull(endInit), breakLoc, continueLoc, returnLoc)) val assume = StmtLabel( Stmts.Assume( AbstractExprs.Eq(testValue.expression, cStatement.expr.expression)), diff --git a/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java b/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java index ebaaf6b539..f8dff80b2b 100644 --- a/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java +++ b/subprojects/xcfa/litmus-cli/src/main/java/hu/bme/mit/theta/xcfa/litmus/cli/LitmusCli.java @@ -117,16 +117,16 @@ private void run() { final Stopwatch sw = Stopwatch.createStarted(); try { - final Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver(); + try (Solver solver = SolverManager.resolveSolverFactory(this.solver).createSolver()) { - final MCM mcm = CatDslManager.createMCM(cat); - logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n"); - final XCFA xcfa = LitmusInterpreter.getXcfa(litmus); - logger.write(Logger.Level.MAINSTEP, "Litmus test parsed successfully\n"); + final MCM mcm = CatDslManager.createMCM(cat); + logger.write(Logger.Level.MAINSTEP, "CAT model parsed successfully\n"); + final XCFA xcfa = LitmusInterpreter.getXcfa(litmus); + logger.write(Logger.Level.MAINSTEP, "Litmus test parsed successfully\n"); - if (printxcfa) { - System.out.println(toDot(xcfa)); - } + if (printxcfa) { + System.out.println(toDot(xcfa)); + } // final List processIds = listToRange(processes, -1, -1); // @@ -151,6 +151,7 @@ private void run() { // mcmSafetyResult.visualize(); // } // } + } } catch (final Throwable t) { t.printStackTrace(); System.exit(-1); @@ -180,4 +181,4 @@ public static void registerAllSolverManagers(String home, Logger logger) throws } } -} \ No newline at end of file +} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt index c6cdf310ce..b57c6028c1 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/ExtensionProperty.kt @@ -25,7 +25,7 @@ fun nullableExtension() = NullableExtensionProperty() class ExtensionProperty : ReadWriteProperty { private val map = IdentityHashMap() - override fun getValue(thisRef: R, property: KProperty<*>) = map[thisRef]!! + override fun getValue(thisRef: R, property: KProperty<*>) = checkNotNull(map[thisRef]) override fun setValue(thisRef: R, property: KProperty<*>, value: T) { map[thisRef] = value } diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java index 049ff85188..a3ba68b78c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/XcfaDistToErrComparator.java @@ -33,7 +33,8 @@ import java.util.Map; import java.util.Optional; -import static com.google.common.base.Preconditions.*; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; /** * A comparator for ArgNodes that is based on the distance from the error @@ -71,9 +72,12 @@ public int compare(final ArgNode n1, } private int getWeightedDistance(final ArgNode node) { - checkArgument(node.getState() instanceof XcfaState && ((XcfaState) node.getState()).getProcesses().size() <= 1, "XcfaState expected with a single process."); - if (((XcfaState) node.getState()).getProcesses().size() == 0) return Integer.MAX_VALUE; - final XcfaState state = (XcfaState) node.getState(); + final var localState = node.getState(); + checkArgument(localState instanceof XcfaState && ((XcfaState) localState).getProcesses().size() <= 1, "XcfaState expected with a single process."); + if (((XcfaState) localState).getProcesses().size() == 0) { + return Integer.MAX_VALUE; + } + final XcfaState state = (XcfaState) localState; final int distanceToError = getDistanceToError(state.getProcesses().get(0).component1().peek()); if (distanceToError == Integer.MAX_VALUE) { return distanceToError; @@ -119,4 +123,4 @@ static Map calculateDistancesToError(final XCFA cfa, fina public String toString() { return getClass().getSimpleName(); } -} \ No newline at end of file +}