diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/LineDirectiveMapping.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/LineDirectiveMapping.java index 1b5ec0b3b90..e5fd7a52722 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/LineDirectiveMapping.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/LineDirectiveMapping.java @@ -40,7 +40,6 @@ public class LineDirectiveMapping { private final TreeMap> mMapping; public LineDirectiveMapping(final String file) { - super(); mMapping = constructLineDirectiveMapping(file); } @@ -104,7 +103,7 @@ public Pair getOriginal(final int lineInTu, final String filena if (floor == null) { return new Pair<>(lineInTu, filename); } - final int distanceToLastLineDirective = (lineInTu - floor.getKey()); + final int distanceToLastLineDirective = lineInTu - floor.getKey(); return new Pair<>(floor.getValue().getFirst() + distanceToLastLineDirective, floor.getValue().getSecond()); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/CLocation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/CLocation.java index ae8b029aeab..181897beae7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/CLocation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/CLocation.java @@ -188,19 +188,17 @@ private IASTNode getMergedNode(final CLocation otherCloc) { return otherNode; } else if (otherNode == null) { return myNode; + } else // we have two nodes and want to merge them; if one of both is a translation unit, we take the other + // one. If both are not translation units, we try to find a common parent + if (myNode instanceof IASTTranslationUnit) { + return otherNode; + } else if (otherNode instanceof IASTTranslationUnit) { + return myNode; } else { - // we have two nodes and want to merge them; if one of both is a translation unit, we take the other - // one. If both are not translation units, we try to find a common parent - if (myNode instanceof IASTTranslationUnit) { - return otherNode; - } else if (otherNode instanceof IASTTranslationUnit) { - return myNode; - } else { - final Collection nodes = new HashSet<>(); - nodes.add(myNode); - nodes.add(otherNode); - return CdtASTUtils.findCommonParent(nodes); - } + final Collection nodes = new HashSet<>(); + nodes.add(myNode); + nodes.add(otherNode); + return CdtASTUtils.findCommonParent(nodes); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/LocationFactory.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/LocationFactory.java index a09296baa9b..806121b73c2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/LocationFactory.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/LocationFactory.java @@ -119,7 +119,7 @@ public CACSLProjectLocation(final Set set) { super(Objects.requireNonNull(set).stream().findAny() .orElseThrow(() -> new IllegalArgumentException("set is empty")).getFilePath(), -1, -1, -1, -1); mFilenames = - Collections.unmodifiableSet(set.stream().map(a -> a.getFilePath()).collect(Collectors.toSet())); + Collections.unmodifiableSet(set.stream().map(IASTTranslationUnit::getFilePath).collect(Collectors.toSet())); } public Set getFilenames() { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java index c9a1d073e52..75505ea85a9 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ACSLHandler.java @@ -704,7 +704,7 @@ public Result visit(final IDispatcher main, final Requires node) { mSpecType = ACSLHandler.SPEC_TYPE.REQUIRES; final ILocation loc = mLocationFactory.createACSLLocation(node); final ExpressionResult exprResult = mExprResultTransformer.transformSwitchRexIntToBool( - ((ExpressionResult) main.dispatch(node.getFormula())), loc, main.getAcslHook()); + (ExpressionResult) main.dispatch(node.getFormula()), loc, main.getAcslHook()); if (!exprResult.getStatements().isEmpty() || !exprResult.getOverapprs().isEmpty()) { throw new UnsupportedSyntaxException(loc, "Requires must be translatable by a single expression"); } @@ -720,7 +720,7 @@ public Result visit(final IDispatcher main, final Requires node) { public Result visit(final IDispatcher main, final Ensures node) { final ILocation loc = mLocationFactory.createACSLLocation(node); final ExpressionResult exprResult = mExprResultTransformer.transformSwitchRexIntToBool( - ((ExpressionResult) main.dispatch(node.getFormula())), loc, main.getAcslHook()); + (ExpressionResult) main.dispatch(node.getFormula()), loc, main.getAcslHook()); if (!exprResult.getStatements().isEmpty() || !exprResult.getOverapprs().isEmpty()) { throw new UnsupportedSyntaxException(loc, "Ensures must be translatable by a single expression"); } @@ -869,7 +869,7 @@ public Result visit(final IDispatcher main, final FreeableExpression node) { resultBuilder.addAllExceptLrValue(rIdc); idx = ExpressionFactory.constructStructAccessExpression(loc, idx, SFO.POINTER_BASE); - final Expression[] idc = new Expression[] { idx }; + final Expression[] idc = { idx }; final Expression arr = // new IdentifierExpression(loc, SFO.VALID); ExpressionFactory.constructIdentifierExpression(loc, @@ -894,7 +894,7 @@ public Result visit(final IDispatcher main, final MallocableExpression node) { resultBuilder.addAllExceptLrValue(rIdc); idx = ExpressionFactory.constructStructAccessExpression(loc, idx, SFO.POINTER_BASE); - final Expression[] idc = new Expression[] { idx }; + final Expression[] idc = { idx }; final Expression arr = ExpressionFactory.constructIdentifierExpression(loc, BoogieType.createArrayType(0, new BoogieType[] { BoogieType.TYPE_INT }, BoogieType.TYPE_INT), SFO.VALID, new DeclarationInformation(StorageClass.GLOBAL, null)); @@ -920,7 +920,7 @@ public Result visit(final IDispatcher main, final ValidExpression node) { resultBuilder.addAllExceptLrValue(rIdc); idx = ExpressionFactory.constructStructAccessExpression(loc, idx, SFO.POINTER_BASE); - final Expression[] idc = new Expression[] { idx }; + final Expression[] idc = { idx }; final Expression arr = ExpressionFactory.constructIdentifierExpression(loc, BoogieType.createArrayType(0, new BoogieType[] { BoogieType.TYPE_INT }, BoogieType.TYPE_INT), SFO.VALID, new DeclarationInformation(StorageClass.GLOBAL, null)); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalIdentifierExpressionsFinder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalIdentifierExpressionsFinder.java index 4fe3b4bd0b2..388d70159ed 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalIdentifierExpressionsFinder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalIdentifierExpressionsFinder.java @@ -10,8 +10,8 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; /** - * Looks for all IdentifierExpressions with a global variable inside a given Expression. - * Note that this will crash if any IdentifierExpression. + * Looks for all IdentifierExpressions with a global variable inside a given Expression. Note that this will crash if + * any IdentifierExpression. * * @author Alexander Nutz (nutz@informatik.uni-freiburg.de) * @@ -32,4 +32,4 @@ public Set getGlobalIdentifierExpressions(final Expression super.processExpression(expr); return Collections.unmodifiableSet(mResult); } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalLhsFinder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalLhsFinder.java index baad1f2532a..a26082c49c0 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalLhsFinder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/BoogieGlobalLhsFinder.java @@ -6,9 +6,8 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; /** - * Looks for a VariableLHS with a global variable inside a given LHS. - * Returns such a VariableLHS if it exists, null otherwise. - * Note that this will crash if the VariableLHS does not contain a DeclarationInformation. + * Looks for a VariableLHS with a global variable inside a given LHS. Returns such a VariableLHS if it exists, null + * otherwise. Note that this will crash if the VariableLHS does not contain a DeclarationInformation. * * @author Alexander Nutz (nutz@informatik.uni-freiburg.de) * @@ -34,4 +33,4 @@ public VariableLHS getGlobalId(final LeftHandSide lhs) { super.processLeftHandSide(lhs); return mResult; } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CExpressionTranslator.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CExpressionTranslator.java index 7ade8a1cc3e..57937d02e57 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CExpressionTranslator.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CExpressionTranslator.java @@ -567,8 +567,8 @@ public Result handlePostfixIncrementAndDecrement(final ILocation loc, final int builder.addAuxVarWithDeclaration(auxvar); // assign the old value to the temporary variable - final LeftHandSide[] tmpAsLhs = new LeftHandSide[] { auxvar.getLhs() }; - final Expression[] oldValue = new Expression[] { exprRes.getLrValue().getValue() }; + final LeftHandSide[] tmpAsLhs = { auxvar.getLhs() }; + final Expression[] oldValue = { exprRes.getLrValue().getValue() }; builder.addStatement(StatementFactory.constructAssignmentStatement(loc, tmpAsLhs, oldValue)); final CType oType = exprRes.getLrValue().getCType().getUnderlyingType(); final RValue tmpRValue = new RValue(auxvar.getExp(), oType); @@ -628,8 +628,8 @@ public Result handlePrefixIncrementAndDecrement(final int prefixOp, final ILocat constructXcrementedValue(loc, builder, oType, op, exprRes.getLrValue().getValue()); // assign the old value to the temporary variable - final LeftHandSide[] tmpAsLhs = new LeftHandSide[] { auxvar.getLhs() }; - final Expression[] newValue = new Expression[] { valueXcremented }; + final LeftHandSide[] tmpAsLhs = { auxvar.getLhs() }; + final Expression[] newValue = { valueXcremented }; builder.addStatement(StatementFactory.constructAssignmentStatement(loc, tmpAsLhs, newValue)); builder.setLrValue(new RValue(valueXcremented, oType, false, false)); @@ -874,8 +874,8 @@ private ExpressionResult constructResultForConditionalOperator(final ILocation l */ private Expression constructXcrementedValue(final ILocation loc, final ExpressionResultBuilder result, final CType ctype, final int op, final Expression value) { - assert op == IASTBinaryExpression.op_plus - || op == IASTBinaryExpression.op_minus : "has to be either minus or plus"; + assert op == IASTBinaryExpression.op_plus || op == IASTBinaryExpression.op_minus + : "has to be either minus or plus"; final Expression valueIncremented; if (ctype instanceof CPointer) { final CPointer cPointer = (CPointer) ctype; @@ -1085,10 +1085,8 @@ private Expression doPointerSubtraction(final ILocation loc, final Expression pt ptr2Offset, mExpressionTranslation.getCTypeOfPointerComponents()); final Expression typesize = mMemoryHandler.calculateSizeOf(loc, pointsToType); final CPrimitive typesizeType = mExpressionTranslation.getCTypeOfPointerComponents(); - final Expression offsetDifferenceDividedByTypesize = - mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_divide, - offsetDifference, mExpressionTranslation.getCTypeOfPointerComponents(), typesize, typesizeType); - return offsetDifferenceDividedByTypesize; + return mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_divide, + offsetDifference, mExpressionTranslation.getCTypeOfPointerComponents(), typesize, typesizeType); } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CTranslationUtil.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CTranslationUtil.java index 66a582424d5..fed1ab8e822 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CTranslationUtil.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CTranslationUtil.java @@ -160,8 +160,7 @@ public static List getConstantDimensionsOfArray(final CArray cArrayType final List result = new ArrayList<>(); while (true) { - result.add(Integer - .parseUnsignedInt(typeSizes.extractIntegerValue(currentArrayType.getBound()).toString())); + result.add(Integer.parseUnsignedInt(typeSizes.extractIntegerValue(currentArrayType.getBound()).toString())); final CType valueType = currentArrayType.getValueType().getUnderlyingType(); if (valueType instanceof CArray) { @@ -178,9 +177,9 @@ public static List getConstantDimensionsOfArray(final CArray cArrayType */ public static boolean isAggregateType(final CType valueTypeRaw) { final CType valueType = valueTypeRaw.getUnderlyingType(); - return (valueType instanceof CStructOrUnion - && (((CStructOrUnion) valueType).isStructOrUnion() == StructOrUnion.STRUCT) - || valueType instanceof CArray); + return valueType instanceof CStructOrUnion + && ((CStructOrUnion) valueType).isStructOrUnion() == StructOrUnion.STRUCT + || valueType instanceof CArray; } public static boolean isAggregateOrUnionType(final CType valueTypeRaw) { @@ -191,7 +190,7 @@ public static boolean isAggregateOrUnionType(final CType valueTypeRaw) { private static boolean isUnionType(final CType valueTypeRaw) { final CType valueType = valueTypeRaw.getUnderlyingType(); return valueType instanceof CStructOrUnion - && (((CStructOrUnion) valueType).isStructOrUnion() == StructOrUnion.UNION); + && ((CStructOrUnion) valueType).isStructOrUnion() == StructOrUnion.UNION; } public static int getConstantFirstDimensionOfArray(final CArray cArrayType, final TypeSizes typeSizes) { @@ -206,8 +205,7 @@ public static int getConstantFirstDimensionOfArray(final CArray cArrayType, fina throw new IllegalArgumentException("This array type is incomplete! Cannot extract actual dimensions."); } - final int dimInt = Integer.parseUnsignedInt(extracted.toString()); - return dimInt; + return Integer.parseUnsignedInt(extracted.toString()); } /** @@ -326,8 +324,8 @@ public static boolean isAuxVarMapComplete(final INameHandler nameHandler, final assert rExprdecl instanceof VariableDeclaration; final VariableDeclaration varDecl = (VariableDeclaration) rExprdecl; - assert varDecl - .getVariables().length == 1 : "there are never two auxvars declared in one declaration, right??"; + assert varDecl.getVariables().length == 1 + : "there are never two auxvars declared in one declaration, right??"; final VarList vl = varDecl.getVariables()[0]; assert vl.getIdentifiers().length == 1 : "there are never two auxvars declared in one declaration, right??"; final String id = vl.getIdentifiers()[0]; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ConstantArrayUtil.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ConstantArrayUtil.java index 039fd2bec47..2366736c3f2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ConstantArrayUtil.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ConstantArrayUtil.java @@ -56,8 +56,8 @@ private ConstantArrayUtil() { public static Expression getConstantArray(final FunctionDeclarations decls, final ILocation loc, final BoogieArrayType arrayType, final Expression constant) { - assert arrayType.getValueType().equals(constant.getType()) : "constant array of type " + arrayType - + " cannot have constant value " + constant; + assert arrayType.getValueType().equals(constant.getType()) + : "constant array of type " + arrayType + " cannot have constant value " + constant; final FunctionDeclaration function = getOrDeclareConstantArrayFunction(decls, arrayType); return new FunctionApplication(loc, arrayType, function.getIdentifier(), new Expression[] { constant }); } @@ -72,8 +72,8 @@ public static FunctionDeclaration getOrDeclareConstantArrayFunction(final Functi final BoogieArrayType type) { return getOrDeclareConstantArrayFunction(decls, type, "~param", new BoogieType[] { type.getValueType() }, valType -> { - assert valType.equals(type.getValueType()) : "constant value of type " + type.getValueType() - + " cannot be used for " + valType; + assert valType.equals(type.getValueType()) + : "constant value of type " + type.getValueType() + " cannot be used for " + valType; return FunctionDeclarations.constructNameForFunctionInParam(0); }); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DataRaceChecker.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DataRaceChecker.java index 1a21d0253c0..a7a2fef27b1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DataRaceChecker.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DataRaceChecker.java @@ -338,9 +338,8 @@ private LeftHandSide createRaceIndicatorLhs(final ILocation loc, final LeftHandS final String name = "#race" + ((VariableLHS) lhs).getIdentifier(); final VariableLHS raceLhs = new VariableLHS(loc, getRaceIndicatorType(lhs.getType()), name, DeclarationInformation.DECLARATIONINFO_GLOBAL); - assert mRaceIndicators.getOrDefault(name, (BoogieType) raceLhs.getType()) - .equals(raceLhs.getType()) : "Ambiguous types for " + name + ": " + mRaceIndicators.get(name) - + " vs. " + raceLhs.getType(); + assert mRaceIndicators.getOrDefault(name, (BoogieType) raceLhs.getType()).equals(raceLhs.getType()) + : "Ambiguous types for " + name + ": " + mRaceIndicators.get(name) + " vs. " + raceLhs.getType(); mRaceIndicators.put(name, (BoogieType) raceLhs.getType()); return raceLhs; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DetermineNecessaryDeclarations.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DetermineNecessaryDeclarations.java index c8334c3623e..000350d2b5f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DetermineNecessaryDeclarations.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/DetermineNecessaryDeclarations.java @@ -320,55 +320,47 @@ public int visit(final IASTDeclaration declaration) { mLocalSymbolTable.put(declaratorName, declaration); addIfNecessaryPrelimInverseDependency(declaration, declaratorName); } - } else { - // we have a local declaration - - /* - * if we use a globally defined type, this introduces a dependency for example in the program ---- - * typedef int _int; struct s { _int i; }; ---- this code section will introduce a dependency struct s - * {...}; --> typedef int _int; - * - * when we visit the declaration _int i; - */ - if (declSpec instanceof IASTElaboratedTypeSpecifier) { - // we have an elaborated type specifier, i.e., something like [struct|union|enum] typename varname - final IASTElaboratedTypeSpecifier elts = (IASTElaboratedTypeSpecifier) declSpec; - final String name = getKindStringFromCompositeOrElaboratedTS(elts) + elts.getName().toString(); - final IASTDeclaration decOfName = mLocalSymbolTable.get(name); - if (decOfName != null) { - // if it is null, it must reference to a local declaration (of the same - // scope..) that we keep anyway - addDependency(mCurrentDeclarationStack.peek(), decOfName); - } else { - // .. or it may reference a global declaration that we haven't seen yet (this may - // overapproximate, as we declare shadowed decls reachable, right?? //TODO: not entirely - // clear.. - mDependencyGraphPreliminaryInverse.put(name, mCurrentDeclarationStack.peek()); - } - } else if (declSpec instanceof IASTNamedTypeSpecifier) { - final IASTNamedTypeSpecifier nts = (IASTNamedTypeSpecifier) declSpec; - final String name = nts.getName().toString(); - final IASTDeclaration decOfName = mLocalSymbolTable.get(name); - if (decOfName != null) { - /* - * if it is null, it must reference to a local declaration (of the same scope..) that we keep - * anyway - */ - addDependency(mCurrentDeclarationStack.peek(), decOfName); - } else { - /* - * .. or it may reference a global declaration that we haven't seen yet (this may - * overapproximate, as we declare shadowed decls reachable, right?? TODO: not entirely clear.. - */ - mDependencyGraphPreliminaryInverse.put(name, mCurrentDeclarationStack.peek()); - } + } else /* + * if we use a globally defined type, this introduces a dependency for example in the program ---- + * typedef int _int; struct s { _int i; }; ---- this code section will introduce a dependency struct + * s {...}; --> typedef int _int; + * + * when we visit the declaration _int i; + */ + if (declSpec instanceof IASTElaboratedTypeSpecifier) { + // we have an elaborated type specifier, i.e., something like [struct|union|enum] typename varname + final IASTElaboratedTypeSpecifier elts = (IASTElaboratedTypeSpecifier) declSpec; + final String name = getKindStringFromCompositeOrElaboratedTS(elts) + elts.getName().toString(); + final IASTDeclaration decOfName = mLocalSymbolTable.get(name); + if (decOfName != null) { + // if it is null, it must reference to a local declaration (of the same + // scope..) that we keep anyway + addDependency(mCurrentDeclarationStack.peek(), decOfName); } else { - addDependency(mCurrentDeclarationStack.peek(), declaration); + // .. or it may reference a global declaration that we haven't seen yet (this may + // overapproximate, as we declare shadowed decls reachable, right?? //TODO: not entirely + // clear.. + mDependencyGraphPreliminaryInverse.put(name, mCurrentDeclarationStack.peek()); } + } else if (declSpec instanceof IASTNamedTypeSpecifier) { + final IASTNamedTypeSpecifier nts = (IASTNamedTypeSpecifier) declSpec; + final String name = nts.getName().toString(); + final IASTDeclaration decOfName = mLocalSymbolTable.get(name); + if (decOfName != null) { + /* + * if it is null, it must reference to a local declaration (of the same scope..) that we keep anyway + */ + addDependency(mCurrentDeclarationStack.peek(), decOfName); + } else { + /* + * .. or it may reference a global declaration that we haven't seen yet (this may overapproximate, + * as we declare shadowed decls reachable, right?? TODO: not entirely clear.. + */ + mDependencyGraphPreliminaryInverse.put(name, mCurrentDeclarationStack.peek()); + } + } else { + addDependency(mCurrentDeclarationStack.peek(), declaration); } - /* - * things we do for both global or local declarations - */ String declSpecName = ""; if (declSpec instanceof IASTSimpleDeclSpecifier) { @@ -422,8 +414,7 @@ public int visit(final IASTDeclaration declaration) { } } mCurrentDeclarationStack.push(funDef); - final int nr = super.visit(declaration); - return nr; + return super.visit(declaration); } else { return super.visit(declaration); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ExplorativeNameVisitor.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ExplorativeNameVisitor.java index b5a736855c4..c8c81c1dc83 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ExplorativeNameVisitor.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/ExplorativeNameVisitor.java @@ -135,4 +135,4 @@ private String toString(final IType type) { } return type + " (" + type.getClass().getSimpleName() + ")"; } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionDeclarations.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionDeclarations.java index 55b8c974555..2a25ce31ea3 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionDeclarations.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionDeclarations.java @@ -63,14 +63,12 @@ public class FunctionDeclarations { public static final String OVERAPPROX_IDENTIFIER = "overapproximation"; public static final String INDEX_IDENTIFIER = "indices"; - /** * See {@link #finish()}. */ private boolean mIsFinished; public FunctionDeclarations(final ITypeHandler typeHandler, final TypeSizes typeSizeConstants) { - super(); mTypeHandler = typeHandler; mTypeSizeConstants = typeSizeConstants; } @@ -119,7 +117,7 @@ public FunctionDeclaration declareFunction(final ILocation loc, final String pre /** * (This class ({@link FunctionDeclarations}) does the naming of function parameters internally. This method exposes - * the naming scheme to the outside.) + * the naming scheme to the outside.) * * @return the name that is used for the out parameter of all {@link FunctionDeclaration}s created by this class */ @@ -129,7 +127,7 @@ public static String constructNameForFunctionOutParam() { /** * (This class ({@link FunctionDeclarations}) does the naming of function parameters internally. This method exposes - * the naming scheme to the outside.) + * the naming scheme to the outside.) * * @return the name that is used for the i-th in parameter of all {@link FunctionDeclaration}s created by this class */ @@ -139,8 +137,8 @@ public static String constructNameForFunctionInParam(final int i) { public LinkedHashMap getDeclaredFunctions() { if (mIsFinished) { - throw new AssertionError("since the map is modifiable we do not allow this query once this class is " - + "finished"); + throw new AssertionError( + "since the map is modifiable we do not allow this query once this class is " + "finished"); } return mDeclaredFunctions; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionTableBuilder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionTableBuilder.java index 5bcb8e69aff..db9fc76bea1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionTableBuilder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionTableBuilder.java @@ -42,7 +42,7 @@ public class FunctionTableBuilder extends ASTVisitor { private final LinkedHashMap mFunctionTable; - + private final FlatSymbolTable mSymTab; public FunctionTableBuilder(final FlatSymbolTable fst) { @@ -65,13 +65,11 @@ public int visit(final IASTDeclaration declaration) { for (final IASTDeclarator d : cd.getDeclarators()) { final String key = d.getName().toString(); final String rslvKey = mSymTab.applyMultiparseRenaming(declaration.getContainingFilename(), key); - if (d instanceof IASTFunctionDeclarator) { - // we only update the table with a declaration, if there is no entry for that name yet. - // otherwise we might only keep the declaration and omit the implementation from - // reachableDeclarations. - if (!mFunctionTable.containsKey(rslvKey)) { - mFunctionTable.put(rslvKey, d); - } + // we only update the table with a declaration, if there is no entry for that name yet. + // otherwise we might only keep the declaration and omit the implementation from + // reachableDeclarations. + if ((d instanceof IASTFunctionDeclarator) && !mFunctionTable.containsKey(rslvKey)) { + mFunctionTable.put(rslvKey, d); } } @@ -82,8 +80,8 @@ public int visit(final IASTDeclaration declaration) { possiblyNestedDeclarator = possiblyNestedDeclarator.getNestedDeclarator(); } final String nameOfInnermostDeclarator = possiblyNestedDeclarator.getName().toString(); - final String rslvName = mSymTab.applyMultiparseRenaming(declaration.getContainingFilename(), - nameOfInnermostDeclarator); + final String rslvName = + mSymTab.applyMultiparseRenaming(declaration.getContainingFilename(), nameOfInnermostDeclarator); mFunctionTable.put(rslvName, declaration); } return super.visit(declaration); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/IDispatcher.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/IDispatcher.java index 0add3649147..eb5bbdfd19a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/IDispatcher.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/IDispatcher.java @@ -94,4 +94,4 @@ public interface IDispatcher { List getFunctionContractFromWitness(IASTNode node); Set getWitnessDeclarations(); -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NameHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NameHandler.java index 017d2f0a039..e70169dd62f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NameHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NameHandler.java @@ -101,7 +101,7 @@ public String getUniqueIdentifier(final IASTNode scope, String cId, final int co } } assert cId.length() > 0 : "Empty C identifier"; - assert (compCnt >= 0); + assert compCnt >= 0; // mark variables that we put on the heap manually (bc they are addressoffed) // with a "#" String onHeapStr = ""; @@ -155,10 +155,10 @@ public String getTempVarUID(final SFO.AUXVAR purpose, final CType cType) { @Override public String getTempVarUIDForBlockScope(final SFO.AUXVAR purpose, final CType cType) { - final String boogieId = SFO.TEMP + purpose.getId() + mTmpUID++; + // do not add it as a temp var since it should not be havocced immediately (at C statement level) // mBacktranslator.putTempVar(boogieId, purpose, cType); - return boogieId; + return SFO.TEMP + purpose.getId() + mTmpUID++; } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NextACSL.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NextACSL.java index 05f17d53289..48d4953435b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NextACSL.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/NextACSL.java @@ -3,27 +3,27 @@ * Copyright (C) 2015 Oleksii Saukh (saukho@informatik.uni-freiburg.de) * Copyright (C) 2015 Stefan Wissert * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ /** @@ -48,19 +48,17 @@ public class NextACSL { */ private final List mAcsl; /** - * The successor C node as reference, where the ACSL is contained in the - * translation unit. + * The successor C node as reference, where the ACSL is contained in the translation unit. */ private final IASTNode mSuccessorCNode; /** * Constructor. - * + * * @param acsl * a list of ACSL comments to hold. * @param successorCNode - * the successor C node as reference, where the ACSL is contained - * in the translation unit. + * the successor C node as reference, where the ACSL is contained in the translation unit. */ public NextACSL(final List acsl, final IASTNode successorCNode) { assert acsl != null; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TranslationSettings.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TranslationSettings.java index 9647b0d4a24..ff934d15ea3 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TranslationSettings.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TranslationSettings.java @@ -30,6 +30,8 @@ */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base; +import java.util.Objects; + import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.exception.UnsupportedSyntaxException; @@ -97,15 +99,13 @@ public TranslationSettings(final IPreferenceProvider ups) { mCheckErrorFunction = ups.getBoolean(CACSLPreferenceInitializer.LABEL_ERROR); mSmtBoolArraysWorkaround = ups.getBoolean(CACSLPreferenceInitializer.LABEL_SMT_BOOL_ARRAYS_WORKAROUND); mCheckIfFreedPointerIsValid = ups.getBoolean(CACSLPreferenceInitializer.LABEL_CHECK_FREE_VALID); - mPointerBaseValidity = - ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_POINTER_VALIDITY, CheckMode.class); + mPointerBaseValidity = ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_POINTER_VALIDITY, CheckMode.class); mPointerTargetFullyAllocated = ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_POINTER_ALLOC, CheckMode.class); // mCheckFreeValid = // prefs.getBoolean(CACSLPreferenceInitializer.LABEL_CHECK_FREE_VALID); - mCheckPointerSubtractionAndComparisonValidity = - ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_POINTER_SUBTRACTION_AND_COMPARISON_VALIDITY, - CheckMode.class); + mCheckPointerSubtractionAndComparisonValidity = ups.getEnum( + CACSLPreferenceInitializer.LABEL_CHECK_POINTER_SUBTRACTION_AND_COMPARISON_VALIDITY, CheckMode.class); mMemoryModelPreference = ups.getEnum(CACSLPreferenceInitializer.LABEL_MEMORY_MODEL, MemoryModel.class); mFpToIeeeBvExtension = ups.getBoolean(CACSLPreferenceInitializer.LABEL_FP_TO_IEEE_BV_EXTENSION); @@ -114,10 +114,10 @@ public TranslationSettings(final IPreferenceProvider ups) { mInRange = ups.getBoolean(CACSLPreferenceInitializer.LABEL_ASSUME_NONDET_VALUES_IN_RANGE); mCheckArrayAccessOffHeap = ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_ARRAYACCESSOFFHEAP, CheckMode.class); - mDivisionByZeroOfIntegerTypes = ups.getEnum( - CACSLPreferenceInitializer.LABEL_CHECK_DIVISION_BY_ZERO_OF_INTEGER_TYPES, CheckMode.class); - mDivisionByZeroOfFloatingTypes = ups.getEnum( - CACSLPreferenceInitializer.LABEL_CHECK_DIVISION_BY_ZERO_OF_FLOATING_TYPES, CheckMode.class); + mDivisionByZeroOfIntegerTypes = + ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_DIVISION_BY_ZERO_OF_INTEGER_TYPES, CheckMode.class); + mDivisionByZeroOfFloatingTypes = + ups.getEnum(CACSLPreferenceInitializer.LABEL_CHECK_DIVISION_BY_ZERO_OF_FLOATING_TYPES, CheckMode.class); mBitpreciseBitfields = ups.getBoolean(CACSLPreferenceInitializer.LABEL_BITPRECISE_BITFIELDS); mBitvectorTranslation = ups.getBoolean(CACSLPreferenceInitializer.LABEL_BITVECTOR_TRANSLATION); mOverapproximateFloatingPointOperations = @@ -367,10 +367,7 @@ public String toString() { @Override public int hashCode() { - final int prime = 31; - int result = 1; - result = prime * result + ((mNewPreferredMemoryModel == null) ? 0 : mNewPreferredMemoryModel.hashCode()); - return result; + return Objects.hash(mNewPreferredMemoryModel); } @Override @@ -391,4 +388,4 @@ public boolean equals(final Object obj) { return true; } } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ArrayHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ArrayHandler.java index 8c1d84240fb..7584ad3dd4b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ArrayHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ArrayHandler.java @@ -285,4 +285,4 @@ private void addArrayBoundsCheckForCurrentIndex(final ILocation loc, final RValu private static boolean isInnermostSubscriptExpression(final IASTArraySubscriptExpression node) { return !(node.getArrayExpression() instanceof IASTArraySubscriptExpression); } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/BaseMemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/BaseMemoryModel.java index 069bdbea7f6..49f356df4fe 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/BaseMemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/BaseMemoryModel.java @@ -115,7 +115,6 @@ public final String getInitPointerProcedureName() { return WRITE_PROCEDURE_PREFIX + INIT_INFIX + hda.getName(); } - public abstract HeapDataArray getDataHeapArray(CPrimitives primitive); public final HeapDataArray getPointerHeapArray() { @@ -138,13 +137,11 @@ public final List getReadWriteDefinitionForHeapDataArray(fi final RequiredMemoryModelFeatures requiredMemoryModelFeatures) { if (hda == mPointerArray) { if (requiredMemoryModelFeatures.isPointerOnHeapRequired()) { - return Collections.singletonList( - new ReadWriteDefinition(getPointerHeapArray().getName(), bytesizeOfStoredPointerComponents(), - getPointerHeapArray().getASTType(), Collections.emptySet(), - requiredMemoryModelFeatures.isPointerUncheckedWriteRequired(), - requiredMemoryModelFeatures.isPointerInitRequired(), - requiredMemoryModelFeatures.isPointerUncheckedReadRequired() - )); + return Collections.singletonList(new ReadWriteDefinition(getPointerHeapArray().getName(), + bytesizeOfStoredPointerComponents(), getPointerHeapArray().getASTType(), Collections.emptySet(), + requiredMemoryModelFeatures.isPointerUncheckedWriteRequired(), + requiredMemoryModelFeatures.isPointerInitRequired(), + requiredMemoryModelFeatures.isPointerUncheckedReadRequired())); } return Collections.emptyList(); } @@ -190,7 +187,6 @@ public String getUncheckedReadProcedureName() { return READ_PROCEDURE_PREFIX + UNCHECKED_PREFIX + mProcedureSuffix; } - public String getWriteProcedureName() { return WRITE_PROCEDURE_PREFIX + mProcedureSuffix; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CCharacterConstant.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CCharacterConstant.java index 6aaac4382c6..498cd96d99b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CCharacterConstant.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CCharacterConstant.java @@ -40,28 +40,25 @@ * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de) */ public class CCharacterConstant { - + /** - * Representation of this character literal in source code. + * Representation of this character literal in source code. */ private final String mSourceLiteral; - - + private final BigInteger mNumericalValue; - - + private final BigInteger mRepresentingValue; - + /** - * The signedness of 'char' determines the representation of the string's - * characters when stored as a sequence of bytes. + * The signedness of 'char' determines the representation of the string's characters when stored as a sequence of + * bytes. */ private final Signedness mSignednessOfChar; - + private final Signedness mSignednessOfRepresentingType; - + private final CPrimitive mType; - public CCharacterConstant(final String sourceLiteral, final Signedness signednessOfChar) { mSourceLiteral = sourceLiteral; @@ -107,7 +104,6 @@ public CCharacterConstant(final String sourceLiteral, final Signedness signednes mRepresentingValue = computeRepresentingValue(mNumericalValue, signednessOfChar, mSignednessOfRepresentingType); } - private BigInteger computeRepresentingValue(final BigInteger numericalValue, final Signedness signednessOfChar, final Signedness signednessOfRepresentingType) { BigInteger result; @@ -124,17 +120,12 @@ private BigInteger computeRepresentingValue(final BigInteger numericalValue, fin } - public BigInteger getRepresentingValue() { return mRepresentingValue; } - public CPrimitive getType() { return mType; } - - - } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CStringLiteral.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CStringLiteral.java index 70edf389c0a..efb46835a79 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CStringLiteral.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/CStringLiteral.java @@ -37,10 +37,9 @@ * *
* - * TODO 20211106 Matthias: Our handling of wchar_t, char16_t and char32_t is - * probably incorrect (especially the mNumericalValues and mByteValues) the aim - * of the current implementation is to umsoundly handle all multibyte characters - * as chars. + * TODO 20211106 Matthias: Our handling of wchar_t, char16_t and char32_t is probably incorrect (especially the + * mNumericalValues and mByteValues) the aim of the current implementation is to umsoundly handle all multibyte + * characters as chars. * * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de) */ @@ -48,7 +47,7 @@ public class CStringLiteral { public enum CharacterType { CHAR, WCHAR_T, CHAR16_T, CHAR32_T - }; + } /** * Type of this string's characters. @@ -107,11 +106,10 @@ public CStringLiteral(final char[] quotedSourceCodeStringLiteral, final Signedne } private String stripQuotes(final char[] chars, final int offset) { - if (chars[offset] == '\"' && chars[chars.length-1] == '\"') { - return new String(chars, offset+1, chars.length-2-offset); + if (chars[offset] == '\"' && chars[chars.length - 1] == '\"') { + return new String(chars, offset + 1, chars.length - 2 - offset); } else { - throw new UnsupportedOperationException( - "unsupported representation of string literal " + chars); + throw new UnsupportedOperationException("unsupported representation of string literal " + chars); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/HeapDataArray.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/HeapDataArray.java index a57e3876102..0b714079730 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/HeapDataArray.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/HeapDataArray.java @@ -29,6 +29,8 @@ */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; +import java.util.Objects; + import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType; @@ -108,12 +110,7 @@ public int getSize() { @Override public int hashCode() { - final int prime = 31; - int result = 1; - result = prime * result + ((mContentASTType == null) ? 0 : mContentASTType.hashCode()); - result = prime * result + ((mName == null) ? 0 : mName.hashCode()); - result = prime * result + mSize; - return result; + return Objects.hash(mContentASTType, mName, mSize); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java index 27cdf23b5c3..bb7718d7f9f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java @@ -200,7 +200,7 @@ public InitializationHandler(final TranslationSettings settings, final MemoryHan public ExpressionResult initialize(final ILocation loc, final LeftHandSide lhsRaw, final CType targetCTypeRaw, final InitializerResult initializerRaw, final IASTNode hook) { final boolean onHeap; - if (lhsRaw != null && lhsRaw instanceof VariableLHS) { + if (lhsRaw instanceof VariableLHS) { onHeap = mCHandler.isHeapVar(((VariableLHS) lhsRaw).getIdentifier()); } else { onHeap = false; @@ -244,9 +244,10 @@ public ExpressionResult initialize(final ILocation loc, final LeftHandSide lhsRa { final boolean nondet = initializerInfo != null && initializerInfo.isMakeNondeterministicInitialization(); - assert !onHeap || !nondet || !initializerInfo.getOverapprs().isEmpty() : "on heap variables get " - + "intitialized to 0, so they are never nondeterministically initialized, except when they are" - + "overapproximated string literals"; + assert !onHeap || !nondet || !initializerInfo.getOverapprs().isEmpty() : """ + on heap variables get \ + intitialized to 0, so they are never nondeterministically initialized, except when they are\ + overapproximated string literals"""; } /* @@ -427,7 +428,7 @@ private ExpressionResult initCStruct(final ILocation loc, final LRValue lhsIfAny final LRValue currentFieldLhs; if (onHeap) { - assert lhsIfAny != null && lhsIfAny instanceof HeapLValue; + assert lhsIfAny instanceof HeapLValue; currentFieldLhs = constructAddressForStructField(loc, (HeapLValue) structBaseLhsToInitialize, i); } else if (lhsIfAny != null) { currentFieldLhs = CTranslationUtil.constructOffHeapStructAccessLhs(loc, @@ -475,7 +476,7 @@ private ExpressionResult initCStruct(final ILocation loc, final LRValue lhsIfAny * constructed for this purpose. */ final List fieldValues = - fieldLrValues.stream().map(fieldLrValue -> fieldLrValue.getValue()).collect(Collectors.toList()); + fieldLrValues.stream().map(LRValue::getValue).collect(Collectors.toList()); final StructConstructor initializationValue = ExpressionFactory.constructStructConstructor(loc, cStructType.getFieldIds(), fieldValues.toArray(new Expression[fieldValues.size()])); @@ -886,7 +887,7 @@ private LRValue obtainLhsToInitialize(final ILocation loc, final LRValue lhsIfAn final boolean onHeap, final ExpressionResultBuilder initialization) { final LRValue arrayLhsToInitialize; if (onHeap) { - assert lhsIfAny != null && lhsIfAny instanceof HeapLValue; + assert lhsIfAny instanceof HeapLValue; arrayLhsToInitialize = lhsIfAny; } else { arrayLhsToInitialize = obtainLocalLValueToInitialize(loc, (LocalLValue) lhsIfAny, cType, initialization); @@ -1203,12 +1204,14 @@ public InitializerInfo constructInitializerInfo(final ILocation loc, final Initi final ExpressionResult exprResult = convertInitResultWithExpressionResult(loc, targetCType, initializerResult, hook); - assert exprResult.getDeclarations().isEmpty() : "the declarations necessary for a StringLiteral " - + " should be registered in StaticObjectsHandler directly (because the need to be global" - + "boogie declarations)"; - assert exprResult.getStatements().isEmpty() : "the statements necessary for a StringLiteral " - + " should be registered in StaticObjectsHandler directly (because the need to be global" - + "boogie declarations)"; + assert exprResult.getDeclarations().isEmpty() : """ + the declarations necessary for a StringLiteral \ + should be registered in StaticObjectsHandler directly (because the need to be global\ + boogie declarations)"""; + assert exprResult.getStatements().isEmpty() : """ + the statements necessary for a StringLiteral \ + should be registered in StaticObjectsHandler directly (because the need to be global\ + boogie declarations)"""; final ExpressionResult onlyRValueExprResult = new ExpressionResultBuilder() .setLrValue(exprResult.getLrValue()).addOverapprox(exprResult.getOverapprs()).build(); @@ -1308,10 +1311,8 @@ private InitializerInfo constructIndexToInitInfo(final ILocation loc, * union type. In the latter case, the initial value of the object, including unnamed members, is that of * the expression. */ - if (rest.peekFirst().isInitializerList() || ( - // TODO: make a more general compatibility check, for example for array and pointer - rest.peekFirst().hasRootExpressionResult() && TypeHandler.isCompatibleType(cellType, - rest.peekFirst().getRootExpressionResult().getLrValue().getCType()))) { + if (rest.peekFirst().isInitializerList() || rest.peekFirst().hasRootExpressionResult() && TypeHandler + .isCompatibleType(cellType, rest.peekFirst().getRootExpressionResult().getLrValue().getCType())) { /* * case "{", i.e. one more brace opens Then the cell is initialized with the list belonging to that * brace (until the matching brace). No residue is taken over if too many elements are left. @@ -1498,8 +1499,8 @@ private static class InitializerInfo { private final List mUnusedListEntries; private InitializerInfo(final ExpressionResult expressionResult, final List rest) { - assert expressionResult.getLrValue() == null - || expressionResult.getLrValue() instanceof RValue : "switch to RValue first!"; + assert expressionResult.getLrValue() == null || expressionResult.getLrValue() instanceof RValue + : "switch to RValue first!"; mExpressionResult = expressionResult; mOverApprs = expressionResult.getOverapprs(); mElementInitInfos = Collections.emptyMap(); @@ -1622,7 +1623,7 @@ public String toString() { public Result handleDesignatedInitializer(final IDispatcher main, final LocationFactory locationFactory, final CASTDesignatedInitializer node) { final ILocation loc = locationFactory.createCLocation(node); - if (node.getDesignators().length == 1 && (node.getDesignators()[0] instanceof CASTFieldDesignator)) { + if (node.getDesignators().length == 1 && node.getDesignators()[0] instanceof CASTFieldDesignator) { // a field designator, as in "struct field" final CASTFieldDesignator fieldDesignator = (CASTFieldDesignator) node.getDesignators()[0]; final String fieldDesignatorName = fieldDesignator.getName().toString(); @@ -1642,7 +1643,7 @@ public Result handleDesignatedInitializer(final IDispatcher main, final Location } else { throw new UnsupportedSyntaxException(loc, "Unexpected result"); } - } else if (node.getDesignators().length == 1 && (node.getDesignators()[0] instanceof CASTArrayDesignator)) { + } else if (node.getDesignators().length == 1 && node.getDesignators()[0] instanceof CASTArrayDesignator) { // designator denotes some field in an array; // one designator means a one-dimensional array "access" (I think) final CASTArrayDesignator arrayDesignator = (CASTArrayDesignator) node.getDesignators()[0]; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/LocalLValueILocationPair.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/LocalLValueILocationPair.java index 7b21e02ca71..beff348817a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/LocalLValueILocationPair.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/LocalLValueILocationPair.java @@ -1,27 +1,27 @@ /* * Copyright (C) 2014-2015 Alexander Nutz (nutz@informatik.uni-freiburg.de) * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; @@ -34,8 +34,7 @@ public class LocalLValueILocationPair { LocalLValue llv; ILocation loc; - public LocalLValueILocationPair(LocalLValue llv, ILocation loc) { - super(); + public LocalLValueILocationPair(final LocalLValue llv, final ILocation loc) { this.llv = llv; this.loc = loc; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModelDeclarations.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModelDeclarations.java index eb87bde18d3..a06a4ced227 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModelDeclarations.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModelDeclarations.java @@ -181,4 +181,4 @@ private static boolean memcpyOrMemmoveRequirements(final RequiredMemoryModelFeat changedSomething |= mmf.require(ULTIMATE_DATA_RACE_MEMORY); return changedSomething; } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel_Unbounded.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel_Unbounded.java index dc36f1cb802..8501d288f73 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel_Unbounded.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel_Unbounded.java @@ -117,7 +117,7 @@ public List getReadWriteDefinitionForNonPointerHeapDataArra final boolean alsoInit = DataStructureUtils .haveNonEmptyIntersection(requiredMemoryModelFeatures.getInitWriteRequired(), primitives); final boolean alsoUncheckedRead = DataStructureUtils - .haveNonEmptyIntersection(requiredMemoryModelFeatures.getUncheckedReadRequired(), primitives); + .haveNonEmptyIntersection(requiredMemoryModelFeatures.getUncheckedReadRequired(), primitives); result.add(new ReadWriteDefinition(procedureName, bytesize, astType, primitives, alsoUncheckedWrite, alsoInit, alsoUncheckedRead)); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/PostProcessor.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/PostProcessor.java index a20dab6f844..1205c23a448 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/PostProcessor.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/PostProcessor.java @@ -222,10 +222,10 @@ public ArrayList postProcess(final ILocation loc, final IASTNode ho mLogger.info("Analyzing all entry points"); if (mProcedureManager.hasProcedure(SFO.MAIN)) { - final String msg = - "You selected the library mode (i.e., each procedure can be starting procedure and global " - + "variables are not initialized). This program contains a \"main\" procedure. Maybe you " - + "wanted to select the \"main\" procedure as starting procedure."; + final String msg = """ + You selected the library mode (i.e., each procedure can be starting procedure and global \ + variables are not initialized). This program contains a "main" procedure. Maybe you \ + wanted to select the "main" procedure as starting procedure."""; mReporter.warn(loc, msg); } } @@ -245,7 +245,7 @@ public ArrayList postProcess(final ILocation loc, final IASTNode ho decl.addAll(declareCurrentRoundingModeVar(loc)); } } - final BvOp[] importantBvOperations = new BvOp[] { BvOp.bvadd, BvOp.bvneg }; + final BvOp[] importantBvOperations = { BvOp.bvadd, BvOp.bvneg }; mExpressionTranslation.declareBinaryBitvectorFunctionsForAllIntegerDatatypes(loc, importantBvOperations); } assert decl.stream().allMatch(Objects::nonNull); @@ -272,7 +272,7 @@ public ArrayList declarePrimitiveDataTypeSynonyms(final ILocation l attributes[1] = new NamedAttribute(loc, "bitsize", new Expression[] { ExpressionFactory.createIntegerLiteral(loc, String.valueOf(bitsize)) }); final String identifier = "C_" + cPrimitive.name(); - final String[] typeParams = new String[0]; + final String[] typeParams = {}; final ASTType astType = mTypeHandler.byteSize2AstType(loc, CPrimitiveCategory.INTTYPE, bytesize); decls.add(new TypeDeclaration(loc, attributes, false, identifier, typeParams, astType)); } @@ -323,7 +323,7 @@ public ArrayList declareFloatDataTypes(final ILocation loc) { ExpressionFactory.createIntegerLiteral(loc, String.valueOf(indices[1])) }); } final String identifier = "C_" + cPrimitive.name(); - final String[] typeParams = new String[0]; + final String[] typeParams = {}; decls.add(new TypeDeclaration(loc, attributes, false, identifier, typeParams)); } return decls; @@ -341,7 +341,7 @@ public ArrayList declareRoundingModeDataTypes(final ILocation loc) attributesRM[0] = new NamedAttribute(loc, FunctionDeclarations.BUILTIN_IDENTIFIER, new Expression[] { ExpressionFactory.createStringLiteral(loc, smtlibRmIdentifier) }); } - final String[] typeParamsRM = new String[0]; + final String[] typeParamsRM = {}; decls.add(new TypeDeclaration(loc, attributesRM, false, BitvectorTranslation.ROUNDING_MODE_BOOGIE_TYPE_IDENTIFIER, typeParamsRM)); @@ -508,7 +508,7 @@ private ArrayList declareConversionFunctions() { final String outInt = "outInt"; final VarList realParam = new VarList(ignoreLoc, new String[] {}, new PrimitiveType(ignoreLoc, BoogieType.TYPE_REAL, SFO.REAL)); - final VarList[] oneRealParam = new VarList[] { realParam }; + final VarList[] oneRealParam = { realParam }; final VarList intParam = new VarList(ignoreLoc, new String[] { outInt }, new PrimitiveType(ignoreLoc, BoogieType.TYPE_INT, SFO.INT)); @@ -676,8 +676,7 @@ id, new DeclarationInformation(StorageClass.IMPLEMENTATION_OUTPARAM, } builder.addAuxVars(firstElseRex.getAuxVars()); - final ArrayList firstElseStmt = new ArrayList<>(); - firstElseStmt.addAll(firstElseRex.getStatements()); + final ArrayList firstElseStmt = new ArrayList<>(firstElseRex.getStatements()); if (!resultTypeIsVoid) { final AssignmentStatement assignment = StatementFactory.constructAssignmentStatement(loc, new VariableLHS[] { auxvar.getLhs() }, diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java index 995a4efdaed..13b91217518 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java @@ -196,7 +196,7 @@ public List computeFinalProcedureDeclarations(final MemoryHandler m */ final ISuccessorProvider successorProvider = x -> mInverseCallGraph.getImage(x).iterator(); final Set allProcedures = new HashSet<>(mProcedureNameToProcedureInfo.values()); - final Function> initialProcToModGlobals = p -> p.getModifiedGlobals(); + final Function> initialProcToModGlobals = BoogieProcedureInfo::getModifiedGlobals; final Map> closedProcToModGlobals = TransitiveClosure.computeClosure(mLogger, allProcedures, initialProcToModGlobals, successorProvider); @@ -462,8 +462,7 @@ public void addSpecificationsToCurrentProcedure(final List specs) final BoogieProcedureInfo procInfo = mCurrentProcedureInfo; final Procedure oldDecl = procInfo.getDeclaration(); - final List newSpecs = new ArrayList<>(); - newSpecs.addAll(Arrays.asList(oldDecl.getSpecification())); + final List newSpecs = new ArrayList<>(Arrays.asList(oldDecl.getSpecification())); newSpecs.addAll(specs); final Procedure newDecl = new Procedure(oldDecl.getLoc(), oldDecl.getAttributes(), oldDecl.getIdentifier(), @@ -486,8 +485,8 @@ public void registerCalledBeforeDeclaredFunction(final BoogieProcedureInfo procI } public Set getAllFunctionSignatures() { - return mProcedureNameToProcedureInfo.entrySet().stream().map(Entry::getValue).filter(x -> x.hasCType()) - .map(x -> x.getCType()).collect(Collectors.toSet()); + return mProcedureNameToProcedureInfo.entrySet().stream().map(Entry::getValue).filter(BoogieProcedureInfo::hasCType) + .map(BoogieProcedureInfo::getCType).collect(Collectors.toSet()); } private static class CallAndAssignmentStatementFinder extends BoogieVisitor { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureSignature.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureSignature.java index 50fa30f0cfa..c13c56f2a8a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureSignature.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureSignature.java @@ -53,9 +53,8 @@ private String buildStringRepresentation() { final StringBuilder sb = new StringBuilder(); sb.append("##fun~"); String times = ""; - for (int i = 0; i < mInParams.size(); i++) { + for (final ASTType inParam : mInParams) { sb.append(times); - final ASTType inParam = mInParams.get(i); flattenASTTypeName(inParam, sb); times = "~X~"; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/RequiredMemoryModelFeatures.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/RequiredMemoryModelFeatures.java index 38459e6e385..3659d33be59 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/RequiredMemoryModelFeatures.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/RequiredMemoryModelFeatures.java @@ -318,9 +318,11 @@ private void checkIsFrozen() { private void checkNotFrozen() { if (mIsFrozen) { - throw new AssertionError("attempt to modify, although this has been frozen already, " - + "note that if some memory model feature relies on another one, this has to be declared in" - + "MemoryModelDeclarations.resolveDependencies(..)" + "perhaps we need to update a method there"); + throw new AssertionError(""" + attempt to modify, although this has been frozen already, \ + note that if some memory model feature relies on another one, this has to be declared in\ + MemoryModelDeclarations.resolveDependencies(..)\ + perhaps we need to update a method there"""); } } @@ -331,4 +333,4 @@ Set getDataOnHeapRequiredUnchecked() { boolean isPointerOnHeapRequiredUnchecked() { return mPointerOnHeapRequired; } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StaticObjectsHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StaticObjectsHandler.java index e09ff58daf5..bbb23308ff1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StaticObjectsHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StaticObjectsHandler.java @@ -221,8 +221,8 @@ public void completeTypeDeclaration(final String incompleteType, final CType com return; } final CDeclaration oldCDec = mTypeDeclarationToCDeclaration.get(oldBoogieDec); - assert oldCDec != null : "We have a Boogie declaration, we should also have a C declaration: " - + oldBoogieDec.getIdentifier(); + assert oldCDec != null + : "We have a Boogie declaration, we should also have a C declaration: " + oldBoogieDec.getIdentifier(); final TypeDeclaration newBoogieDec = new TypeDeclaration(oldBoogieDec.getLocation(), oldBoogieDec.getAttributes(), oldBoogieDec.isFinite(), oldBoogieDec.getIdentifier(), @@ -245,8 +245,6 @@ public void addGlobalVarDeclarationWithoutCDeclaration(final VariableDeclaration public void addStatementsForUltimateInit(final List stmts) { assert !mIsFrozen; - for (final Statement stmt : stmts) { - mStatementsForUltimateInit.add(stmt); - } + mStatementsForUltimateInit.addAll(stmts); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java index 86360402bfb..b0fbc4e7a69 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java @@ -107,9 +107,9 @@ public Result handleFieldReference(final IDispatcher main, final ExpressionResul fieldOwner.getNeighbourUnionFields() == null ? new ArrayList<>() : new ArrayList<>(fieldOwner.getNeighbourUnionFields()); - final CType foType = (node.isPointerDereference() - ? ((CPointer) fieldOwner.getLrValue().getUnderlyingType()).getPointsToType() - : fieldOwner.getLrValue().getUnderlyingType()); + final CType foType = + node.isPointerDereference() ? ((CPointer) fieldOwner.getLrValue().getUnderlyingType()).getPointsToType() + : fieldOwner.getLrValue().getUnderlyingType(); final CStructOrUnion cStructType = (CStructOrUnion) foType.getUnderlyingType(); final CType cFieldType = cStructType.getFieldType(field); @@ -148,8 +148,8 @@ public Result handleFieldReference(final IDispatcher main, final ExpressionResul newValue = LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, cFieldType, bi); if (cStructType.isStructOrUnion() == StructOrUnion.UNION) { - unionFieldToCType.addAll(computeNeighbourFieldsOfUnionField(loc, field, unionFieldToCType, cStructType, - fieldOwnerHlv)); + unionFieldToCType.addAll( + computeNeighbourFieldsOfUnionField(loc, field, unionFieldToCType, cStructType, fieldOwnerHlv)); } } else if (fieldOwner.getLrValue() instanceof RValue) { final RValue rVal = (RValue) fieldOwner.getLrValue(); @@ -163,8 +163,8 @@ public Result handleFieldReference(final IDispatcher main, final ExpressionResul newValue = new LocalLValue(slhs, cFieldType, bi); if (cStructType.isStructOrUnion() == StructOrUnion.UNION) { - unionFieldToCType.addAll( - computeNeighbourFieldsOfUnionField(loc, field, unionFieldToCType, cStructType, lVal)); + unionFieldToCType + .addAll(computeNeighbourFieldsOfUnionField(loc, field, unionFieldToCType, cStructType, lVal)); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java index 01be12a8d7b..714074f341a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java @@ -209,8 +209,7 @@ private SizeTValue constructSizeTValueArray(final ILocation loc, final CArray cA final SizeTValue valueSize = computeSize(loc, cArray.getValueType()); final SizeTValue factor = extractSizeTValue(cArray.getBound()); - final SizeTValue size = (new SizeTValueAggregatorMultiply()).aggregate(loc, - Arrays.asList(new SizeTValue[] { valueSize, factor })); + final SizeTValue size = new SizeTValueAggregatorMultiply().aggregate(loc, Arrays.asList(valueSize, factor)); if (!mPreferConstantsOverValues) { return size; } @@ -470,7 +469,7 @@ public String toString() { } } - private class SizeTValueExpression implements SizeTValue { + private static class SizeTValueExpression implements SizeTValue { private final Expression mValue; public SizeTValueExpression(final Expression value) { @@ -497,7 +496,7 @@ public Offset(final SizeTValueInteger addressOffset, final int startBit, final i mAddressOffset = addressOffset; mStartBit = startBit; mBitsize = bitsize; - assert (startBit == -1 && bitsize == -1) || (startBit >= 0 && bitsize >= 0); + assert startBit == -1 && bitsize == -1 || startBit >= 0 && bitsize >= 0; } public Expression getAddressOffsetAsExpression(final ILocation loc) { @@ -531,7 +530,7 @@ public String toString() { private Offset computeMemberOffset(final Offset precedingMemberOffset, final CType precedingMemberType, final int bitfieldSize, final ILocation loc) { - final boolean currentMemberIsBitfield = (bitfieldSize != -1); + final boolean currentMemberIsBitfield = bitfieldSize != -1; if (precedingMemberOffset.isBitfieldOffset()) { if (precedingMemberOffset.getBitFieldSize() == 0) { throw new UnsupportedOperationException("Bitfields: case that previous is zero not yet implemented."); @@ -573,7 +572,7 @@ private SizeTValue computeOffsetOfNextByte(final Offset offset, final CType prec return new SizeTValueInteger(offset.getAddressOffset().getInteger().add(BigInteger.ONE)); } final int lastOccupiedBit = offset.getStartBit() + offset.getBitFieldSize(); - final int additionalByes = (lastOccupiedBit / 8) + 1; + final int additionalByes = lastOccupiedBit / 8 + 1; return new SizeTValueInteger(offset.getAddressOffset().getInteger().add(BigInteger.valueOf(additionalByes))); } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java index 4f8b4c9cdb3..7adbc2e9839 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java @@ -97,8 +97,8 @@ public List declareMemcpyOrMemmove(final CHandler main, mTypeHandler.cType2AstType(ignoreLoc, mTypeSizeAndOffsetComputer.getSizeT())); final VarList outP = new VarList(ignoreLoc, new String[] { SFO.RES }, mTypeHandler.constructPointerType(ignoreLoc)); - final VarList[] inParams = new VarList[] { inPDest, inPSrc, inPSize }; - final VarList[] outParams = new VarList[] { outP }; + final VarList[] inParams = { inPDest, inPSrc, inPSize }; + final VarList[] outParams = { outP }; { final Procedure memCpyProcDecl = new Procedure(ignoreLoc, new Attribute[0], memCopyOrMemMove.getName(), @@ -313,4 +313,4 @@ destId, new RValue(loopCtrAux.getExp(), mExpressionTranslation.getCTypeOfPointer return loopBody.build(); } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructRealloc.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructRealloc.java index ba0d44ad9ca..3ba1a69cf0e 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructRealloc.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructRealloc.java @@ -121,8 +121,8 @@ public List declareRealloc(final CHandler main, final Collection declareRealloc(final CHandler main, final Collection constructOverflowCheckForArithmeticExpressio final Expression extendedRhsOperand = extend(loc, rhsOperand, ExtendOperation.sign_extend, inputBitsize, requiredBitsize); declareBitvectorFunctionForArithmeticOperation(loc, bvop, requiredBitsize); - final Expression opResult = BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, - new Expression[] { extendedLhsOperand, extendedRhsOperand }); + final Expression opResult = + BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, extendedLhsOperand, extendedRhsOperand); final Expression biggerMinInt = constructBiggerMinIntConstraint(loc, resultType, requiredBitsize, opResult); final Expression smallerMaxInt = constructSmallerMaxIntConstraint(loc, resultType, requiredBitsize, opResult); return new Pair<>(biggerMinInt, smallerMaxInt); @@ -1552,9 +1550,7 @@ private Expression constructSmallerMaxIntConstraint(final ILocation loc, final C final BvOp operator = mTypeSizes.isUnsigned(resultType) ? BvOp.bvule : BvOp.bvsle; final BigInteger maxValueAsInt = mTypeSizes.getMaxValueOfPrimitiveType(resultType); final Expression maxValueAsExpr = ExpressionFactory.createBitvecLiteral(loc, maxValueAsInt, requiredBitsize); - final Expression smallerMaxInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, operator, - new Expression[] { opResult, maxValueAsExpr }); - return smallerMaxInt; + return BitvectorFactory.constructBinaryBitvectorOperation(loc, operator, opResult, maxValueAsExpr); } private Expression constructBiggerMinIntConstraint(final ILocation loc, final CPrimitive resultType, @@ -1563,9 +1559,7 @@ private Expression constructBiggerMinIntConstraint(final ILocation loc, final CP declareBitvectorFunctionForComparisonOperation(loc, operator, requiredBitsize); final BigInteger minValueAsInt = mTypeSizes.getMinValueOfPrimitiveType(resultType); final Expression minValueAsExpr = ExpressionFactory.createBitvecLiteral(loc, minValueAsInt, requiredBitsize); - final Expression biggerMinInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, operator, - new Expression[] { minValueAsExpr, opResult }); - return biggerMinInt; + return BitvectorFactory.constructBinaryBitvectorOperation(loc, operator, minValueAsExpr, opResult); } private static int computeBitsize(final ASTType type) { @@ -1625,8 +1619,8 @@ protected Pair constructOverflowCheckForLeftShift(final final Expression extendedRhsOperand = extend(loc, rhsOperand, ExtendOperation.sign_extend, inputBitsize, requiredBitsize); declareBitvectorFunctionForArithmeticOperation(loc, bvop, requiredBitsize); - final Expression opResult = BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, - new Expression[] { extendedLhsOperand, extendedRhsOperand }); + final Expression opResult = + BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, extendedLhsOperand, extendedRhsOperand); final Expression biggerMinInt = constructBiggerMinIntConstraint(loc, resultType, requiredBitsize, opResult); final Expression smallerMaxInt = constructSmallerMaxIntConstraint(loc, resultType, requiredBitsize, opResult); return new Pair<>(biggerMinInt, smallerMaxInt); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java index 45a9ae0a47b..b0724aa8fa7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatFunction.java @@ -70,7 +70,6 @@ public class FloatFunction { private final String mTypeSuffix; public FloatFunction(final String prefix, final String function, final String typeSuffix) { - super(); mPrefix = prefix; mFunction = function; mTypeSuffix = typeSuffix; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatSupportInUltimate.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatSupportInUltimate.java index 1e8dce69083..262a8052bbc 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatSupportInUltimate.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/FloatSupportInUltimate.java @@ -43,7 +43,7 @@ public class FloatSupportInUltimate { //@formatter:off - private final static String[] SUPPORTED_FLOAT_OPERATIONS_ARRAY = new String[] { + private final static String[] SUPPORTED_FLOAT_OPERATIONS_ARRAY = { "sqrt", "__isinf", "__finite", @@ -119,7 +119,7 @@ public class FloatSupportInUltimate { "fesetround", }; - private final static String[] UNSUPPORTED_FLOAT_OPERATIONS_ARRAY = new String[] { + private final static String[] UNSUPPORTED_FLOAT_OPERATIONS_ARRAY = { // from math.h "frexp", "ldexp", @@ -369,4 +369,4 @@ public static Set getSupportedFloatOperations() { public static Map getOverapproximatedUnaryFunctions() { return OVERAPPROXIMATED_UNARY_FUNCTIONS; } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IPointerIntegerConversion.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IPointerIntegerConversion.java index c95cebbb43c..4145cd03a13 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IPointerIntegerConversion.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IPointerIntegerConversion.java @@ -37,4 +37,4 @@ public interface IPointerIntegerConversion { ExpressionResult convertIntToPointer(ILocation loc, ExpressionResult rexp, CPointer newType); -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java index f2dedf88d8e..41443d60b09 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java @@ -265,14 +265,14 @@ private Expression constructDivExpression(final ILocation loc, final Expression final CPrimitive leftType, final CPrimitive rightType) { final BigInteger leftValue = mTypeSizes.extractIntegerValue(left, leftType); final BigInteger rightValue = mTypeSizes.extractIntegerValue(right, rightType); - if ((leftValue != null && leftValue.signum() == 0) || BigInteger.ONE.equals(rightValue)) { + if (leftValue != null && leftValue.signum() == 0 || BigInteger.ONE.equals(rightValue)) { return left; } if (leftValue != null && rightValue != null) { return ExpressionFactory.createIntegerLiteral(loc, leftValue.divide(rightValue).toString()); } final Expression normalDivision = ExpressionFactory.newBinaryExpression(loc, Operator.ARITHDIV, left, right); - if (mTypeSizes.isUnsigned(leftType) || (leftValue != null && leftValue.signum() > 0)) { + if (mTypeSizes.isUnsigned(leftType) || leftValue != null && leftValue.signum() > 0) { return normalDivision; } /* @@ -315,7 +315,7 @@ private Expression constructModExpression(final ILocation loc, final Expression return ExpressionFactory.createIntegerLiteral(loc, constantResult); } final Expression normalModulo = ExpressionFactory.newBinaryExpression(loc, Operator.ARITHMOD, left, right); - if (mTypeSizes.isUnsigned(leftType) || (leftValue != null && leftValue.signum() > 0)) { + if (mTypeSizes.isUnsigned(leftType) || leftValue != null && leftValue.signum() > 0) { return normalModulo; } /* @@ -742,8 +742,8 @@ public ExpressionResult constructBuiltinFesetround(final ILocation loc, final Ex public Pair constructOverflowCheckForArithmeticExpression(final ILocation loc, final int operation, final CPrimitive resultType, final Expression lhsOperand, final Expression rhsOperand) { - assert resultType.isIntegerType() - && !mTypeSizes.isUnsigned(resultType) : "Overflow check only for signed integer types"; + assert resultType.isIntegerType() && !mTypeSizes.isUnsigned(resultType) + : "Overflow check only for signed integer types"; assert List.of(IASTBinaryExpression.op_multiply, IASTBinaryExpression.op_multiplyAssign, IASTBinaryExpression.op_plus, IASTBinaryExpression.op_plusAssign, IASTBinaryExpression.op_minus, IASTBinaryExpression.op_minusAssign, IASTBinaryExpression.op_divide, @@ -757,8 +757,8 @@ public Pair constructOverflowCheckForArithmeticExpressio @Override public Pair constructOverflowCheckForUnaryExpression(final ILocation loc, final int operation, final CPrimitive resultType, final Expression operand) { - assert resultType.isIntegerType() - && !mTypeSizes.isUnsigned(resultType) : "Overflow check only for signed integer types"; + assert resultType.isIntegerType() && !mTypeSizes.isUnsigned(resultType) + : "Overflow check only for signed integer types"; assert operation == IASTUnaryExpression.op_minus; final Expression operationResult = constructUnaryExpression(loc, operation, operand, resultType); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/OverapproximationUF.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/OverapproximationUF.java index 00df6760a73..bd2e7d25f80 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/OverapproximationUF.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/OverapproximationUF.java @@ -114,7 +114,7 @@ private String declareConvertIntToPointerFunction(final ILocation loc, final CPr if (!mFunctionDeclarations.getDeclaredFunctions().containsKey(prefixedFunctionName)) { final Attribute attribute = new NamedAttribute(loc, FunctionDeclarations.OVERAPPROX_IDENTIFIER, new Expression[] { ExpressionFactory.createStringLiteral(loc, functionName) }); - final Attribute[] attributes = new Attribute[] { attribute }; + final Attribute[] attributes = { attribute }; final ASTType resultASTType = mTypeHandler.constructPointerType(loc); final ASTType paramASTType = mTypeHandler.cType2AstType(loc, newType); mFunctionDeclarations.declareFunction(loc, prefixedFunctionName, attributes, resultASTType, paramASTType); @@ -128,7 +128,7 @@ private String declareConvertPointerToIntFunction(final ILocation loc, final CPr if (!mFunctionDeclarations.getDeclaredFunctions().containsKey(prefixedFunctionName)) { final Attribute attribute = new NamedAttribute(loc, FunctionDeclarations.OVERAPPROX_IDENTIFIER, new Expression[] { ExpressionFactory.createStringLiteral(loc, functionName) }); - final Attribute[] attributes = new Attribute[] { attribute }; + final Attribute[] attributes = { attribute }; final ASTType resultASTType = mTypeHandler.cType2AstType(loc, newType); final ASTType paramASTType = mTypeHandler.constructPointerType(loc); mFunctionDeclarations.declareFunction(loc, prefixedFunctionName, attributes, resultASTType, paramASTType); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/standardfunctions/ThreadIdManager.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/standardfunctions/ThreadIdManager.java index c57af96ce04..ef1792b9ec6 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/standardfunctions/ThreadIdManager.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/standardfunctions/ThreadIdManager.java @@ -131,8 +131,10 @@ public Expression[] updateForkedThreadId(final IASTInitializerClause argument, f final Expression threadId = getOldForkCounterAsTemp(loc, erb); incrementForkCounter(loc, erb); - final ExpressionResult pointerLValue = mExpressionResultTransformer.dispatchPointerLValue(dispatcher, loc, argument); - erb.addAllExceptLrValue(pointerLValue, mExpressionResultTransformer.makePointerAssignment(loc, pointerLValue.getLrValue(), threadId)); + final ExpressionResult pointerLValue = + mExpressionResultTransformer.dispatchPointerLValue(dispatcher, loc, argument); + erb.addAllExceptLrValue(pointerLValue, + mExpressionResultTransformer.makePointerAssignment(loc, pointerLValue.getLrValue(), threadId)); if (UNAMBIGUOUS_THREAD_ID_OPTIMIZATION) { final Integer unambiguousId = getUnambiguousThreadIdCounter(argument); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfo.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfo.java index 77103d66e84..beed5a27df7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfo.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfo.java @@ -45,8 +45,8 @@ public class AuxVarInfo { public AuxVarInfo(final VariableDeclaration varDec, final VariableLHS lhs, final IdentifierExpression exp) { assert varDec.getVariables().length == 1 : "we allow precisely one identifier per aux var at the moment"; - assert varDec.getVariables()[0].getIdentifiers().length == 1 : "we allow precisely one identifier per aux var " - + "at the moment"; + assert varDec.getVariables()[0].getIdentifiers().length == 1 + : "we allow precisely one identifier per aux var " + "at the moment"; mVarDec = varDec; mLhs = lhs; mExp = exp; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfoBuilder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfoBuilder.java index 1e5e1ff0f42..3c92e0171d1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfoBuilder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/AuxVarInfoBuilder.java @@ -106,7 +106,6 @@ private AuxVarInfo constructAuxVarHelper(final ILocation loc, final String id, f final VariableDeclaration decl = new VariableDeclaration(loc, new Attribute[0], new VarList[] { new VarList(loc, new String[] { id }, astType) }); - final VariableLHS lhs = ExpressionFactory.constructVariableLHS(loc, mTypeHandler.getBoogieTypeForBoogieASTType(astType), id, declInfo); @@ -118,8 +117,7 @@ private AuxVarInfo constructAuxVarHelper(final ILocation loc, final String id, f /** * Normal aux vars are havocced as soon as possible (once we arrive at "statement level" in the translated C - * program). - * Some aux vars are havocced only when the scope (procedure) is left + * program). Some aux vars are havocced only when the scope (procedure) is left * * @param loc * @param cType @@ -127,10 +125,10 @@ private AuxVarInfo constructAuxVarHelper(final ILocation loc, final String id, f * @param compoundliteral * @return */ - public AuxVarInfo constructAuxVarInfoForBlockScope(final ILocation loc, final CType cType, - final AUXVAR auxVarType, final DeclarationInformation declInfo) { - assert auxVarType == SFO.AUXVAR.COMPOUNDLITERAL : "only block-scope aux vars are allowed here (extend the " - + "assertion if you added a new one)"; + public AuxVarInfo constructAuxVarInfoForBlockScope(final ILocation loc, final CType cType, final AUXVAR auxVarType, + final DeclarationInformation declInfo) { + assert auxVarType == SFO.AUXVAR.COMPOUNDLITERAL + : "only block-scope aux vars are allowed here (extend the " + "assertion if you added a new one)"; final String id = mNameHandler.getTempVarUIDForBlockScope(auxVarType, cType); final ASTType astType = mTypeHandler.cType2AstType(loc, cType); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/SymbolTableValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/SymbolTableValue.java index 8f53f683ca7..87fd14873a5 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/SymbolTableValue.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/SymbolTableValue.java @@ -112,8 +112,8 @@ public SymbolTableValue(final String bId, final Declaration boogieDecl, final AS * that expression here. Example: enum entries are translated to Boogie variables, and they have a * constant integer value (which is stored in an axiom elsewhere) */ - public SymbolTableValue(final String bId, final Declaration boogieDecl, final ASTType astType, final CDeclaration cdecl, - final DeclarationInformation declarationInformation, final IASTNode declNode, + public SymbolTableValue(final String bId, final Declaration boogieDecl, final ASTType astType, + final CDeclaration cdecl, final DeclarationInformation declarationInformation, final IASTNode declNode, final boolean isIntFromPointer, final Expression constantValue) { assert bId != null && !bId.equals(SFO.EMPTY); assert cdecl != null; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CArray.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CArray.java index f7b4f847df2..d73e2dd96c8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CArray.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CArray.java @@ -134,9 +134,8 @@ public boolean isIncomplete() { public int hashCode() { final int prime = 31; int result = super.hashCode(); - result = prime * result + ((mBound == null) ? 0 : mBound.hashCode()); - result = prime * result + ((mValueType == null) ? 0 : mValueType.hashCode()); - return result; + result = prime * result + (mBound == null ? 0 : mBound.hashCode()); + return prime * result + (mValueType == null ? 0 : mValueType.hashCode()); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CEnum.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CEnum.java index 4b9fc91fe36..283b374d346 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CEnum.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CEnum.java @@ -143,10 +143,9 @@ public static CType replaceEnumWithInt(final CType cType) { public int hashCode() { final int prime = 31; int result = super.hashCode(); - result = prime * result + ((mIdentifier == null) ? 0 : mIdentifier.hashCode()); + result = prime * result + (mIdentifier == null ? 0 : mIdentifier.hashCode()); result = prime * result + (mIsComplete ? 1231 : 1237); - result = prime * result + Arrays.hashCode(mNames); - return result; + return prime * result + Arrays.hashCode(mNames); } @Override @@ -160,14 +159,14 @@ public boolean equals(final Object o) { } final CEnum oEnum = (CEnum) oType; - if (!(mIdentifier.equals(oEnum.mIdentifier))) { + if (!mIdentifier.equals(oEnum.mIdentifier)) { return false; } if (mNames.length != oEnum.mNames.length) { return false; } for (int i = mNames.length - 1; i >= 0; --i) { - if (!(mNames[i].equals(oEnum.mNames[i]))) { + if (!mNames[i].equals(oEnum.mNames[i])) { return false; } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CFunction.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CFunction.java index 55a236965d8..e90e5e6004e 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CFunction.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CFunction.java @@ -66,8 +66,8 @@ private CFunction(final boolean isConst, final boolean isInline, final boolean i mTakesVarArgs = takesVarArgs; mVarArgsUsage = varArgsUsage; assert mVarArgsUsage != VarArgsUsage.USED || mTakesVarArgs : "Cannot use varargs but not have varargs"; - assert mVarArgsUsage == VarArgsUsage.UNUSED - || mTakesVarArgs : "Cannot have no varargs and not know about usage"; + assert mVarArgsUsage == VarArgsUsage.UNUSED || mTakesVarArgs + : "Cannot have no varargs and not know about usage"; } /** @@ -203,8 +203,8 @@ public VarArgsUsage getVarArgsUsage() { public String toString() { final StringBuilder sb = new StringBuilder(); sb.append("(("); - for (int i = 0; i < mParamTypes.length; i++) { - appendCType(sb, mParamTypes[i].getType()); + for (final CDeclaration mParamType : mParamTypes) { + appendCType(sb, mParamType.getType()); sb.append(" "); } if (mTakesVarArgs) { @@ -230,9 +230,9 @@ public String functionSignatureAsProcedureName() { final StringBuilder sb = new StringBuilder(); sb.append("##fun~"); String times = ""; - for (int i = 0; i < mParamTypes.length; i++) { + for (final CDeclaration mParamType : mParamTypes) { sb.append(times); - sb.append(mParamTypes[i].getType().getUnderlyingType().toString()); + sb.append(mParamType.getType().getUnderlyingType().toString()); times = "~X~"; } if (mTakesVarArgs) { @@ -254,9 +254,8 @@ public int hashCode() { final int prime = 31; int result = super.hashCode(); result = prime * result + Arrays.hashCode(mParamTypes); - result = prime * result + ((mResultType == null) ? 0 : mResultType.hashCode()); - result = prime * result + (mTakesVarArgs ? 1231 : 1237); - return result; + result = prime * result + (mResultType == null ? 0 : mResultType.hashCode()); + return prime * result + (mTakesVarArgs ? 1231 : 1237); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CNamed.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CNamed.java index a6f9663154a..8968abc05bc 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CNamed.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CNamed.java @@ -110,9 +110,8 @@ public boolean isIncomplete() { public int hashCode() { final int prime = 31; int result = super.hashCode(); - result = prime * result + ((mMappedType == null) ? 0 : mMappedType.hashCode()); - result = prime * result + ((mName == null) ? 0 : mName.hashCode()); - return result; + result = prime * result + (mMappedType == null ? 0 : mMappedType.hashCode()); + return prime * result + (mName == null ? 0 : mName.hashCode()); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPointer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPointer.java index dca91ba0a7b..3e480ef0bd7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPointer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPointer.java @@ -94,8 +94,7 @@ public String toString() { public int hashCode() { final int prime = 31; int result = super.hashCode(); - result = prime * result + ((mPointsToType == null) ? 0 : mPointsToType.hashCode()); - return result; + return prime * result + (mPointsToType == null ? 0 : mPointsToType.hashCode()); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPrimitive.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPrimitive.java index 393dbb38239..3b3592710fa 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPrimitive.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CPrimitive.java @@ -312,8 +312,7 @@ public int hashCode() { final int prime = 31; int result = super.hashCode(); result = prime * result + (mGeneralType == null ? 0 : mGeneralType.hashCode()); - result = prime * result + (mType == null ? 0 : mType.hashCode()); - return result; + return prime * result + (mType == null ? 0 : mType.hashCode()); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CType.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CType.java index 19b39e18507..82f33b73291 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CType.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CType.java @@ -31,6 +31,8 @@ */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c; +import java.util.Objects; + import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitiveCategory; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; @@ -114,7 +116,7 @@ public CType getUnderlyingType() { */ public boolean isIntegerType() { if (this instanceof CPrimitive) { - return (((CPrimitive) this).getGeneralType() == CPrimitiveCategory.INTTYPE); + return ((CPrimitive) this).getGeneralType() == CPrimitiveCategory.INTTYPE; } return this instanceof CEnum; } @@ -149,7 +151,7 @@ public boolean isComplexType() { */ public boolean isFloatingType() { if (this instanceof CPrimitive) { - return (((CPrimitive) this).getGeneralType() == CPrimitiveCategory.FLOATTYPE); + return ((CPrimitive) this).getGeneralType() == CPrimitiveCategory.FLOATTYPE; } return false; } @@ -172,7 +174,7 @@ public boolean isArithmeticType() { * Returns true iff this type is a scalar type according to the definition 6.2.5.21 in the C11 standard. */ public boolean isScalarType() { - return (this instanceof CPointer) || isArithmeticType(); + return this instanceof CPointer || isArithmeticType(); } public boolean isVoidPointerType() { @@ -186,14 +188,7 @@ public boolean isVoidType() { @Override public int hashCode() { - final int prime = 31; - int result = 1; - result = prime * result + (mIsConst ? 1231 : 1237); - result = prime * result + (mIsExtern ? 1231 : 1237); - result = prime * result + (mIsInline ? 1231 : 1237); - result = prime * result + (mIsRestrict ? 1231 : 1237); - result = prime * result + (mIsVolatile ? 1231 : 1237); - return result; + return Objects.hash(mIsConst, mIsExtern, mIsInline, mIsRestrict, mIsVolatile); } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/BitfieldInformation.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/BitfieldInformation.java index 397f5ddefbf..79807e24e7a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/BitfieldInformation.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/BitfieldInformation.java @@ -1,35 +1,35 @@ /* * Copyright (C) 2017 Matthias Heizmann (heizmann@informatik.uni-freiburg.de) * Copyright (C) 2017 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result; /** - * Store information about bitfields. - * Currently only the size, but in the future maybe also information about - * the alignment. + * Store information about bitfields. Currently only the size, but in the future maybe also information about the + * alignment. + * * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de) * */ @@ -38,14 +38,11 @@ public class BitfieldInformation { private final int mNumberOfBits; public BitfieldInformation(final int numberOfBits) { - super(); mNumberOfBits = numberOfBits; } public int getNumberOfBits() { return mNumberOfBits; } - - } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/CStorageClass.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/CStorageClass.java index 2ae025f8f5d..c7f7f487d6a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/CStorageClass.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/CStorageClass.java @@ -2,10 +2,9 @@ /** * Enum representing the C storageclass (e.g. typedef,..) of the SymbolTableValue + * * @author nutz */ public enum CStorageClass { - AUTO, EXTERN, /*LAST,*/ MUTABLE, REGISTER, STATIC, TYPEDEF, UNSPECIFIED + AUTO, EXTERN, /* LAST, */ MUTABLE, REGISTER, STATIC, TYPEDEF, UNSPECIFIED } - - diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ContractResult.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ContractResult.java index 9d7a95413e2..19495438de5 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ContractResult.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ContractResult.java @@ -48,7 +48,8 @@ public class ContractResult extends Result { /** * Constructor. * - * @param specs a specification array. + * @param specs + * a specification array. */ public ContractResult(final Specification[] specs) { super(null); @@ -59,5 +60,4 @@ public Specification[] getSpecs() { return specs; } - } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultBuilder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultBuilder.java index 8c3dfb37eec..da5b383eb68 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultBuilder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultBuilder.java @@ -102,9 +102,8 @@ public ExpressionResultBuilder addStatements(final Collect } /** - * Transfer {@link Overapprox} from this object to the statements that is added. - * Note that the {@link Overapprox} are intentionally deleted because they - * should be only added to the translation of the overapproximated code and + * Transfer {@link Overapprox} from this object to the statements that is added. Note that the {@link Overapprox} + * are intentionally deleted because they should be only added to the translation of the overapproximated code and * should not be passed downwards in the AST. */ public ExpressionResultBuilder addStatementAndAnnotateOverapprox(final Statement stm) { @@ -305,4 +304,4 @@ public void clearAuxVars() { mAuxVars.clear(); } -} \ No newline at end of file +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java index ebbf90d99a6..c9561869390 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java @@ -117,7 +117,7 @@ public enum Transformation { CONVERT_NULL_POINTER_TO_CONSTANT( (ert, expr, ttype, loc, hook) -> ert.convertNullPointerConstantToPointer(expr, ttype, loc)); - private ITransformationFunction mFun; + private final ITransformationFunction mFun; Transformation(final ITransformationFunction fun) { mFun = Objects.requireNonNull(fun); @@ -432,9 +432,8 @@ private ExpressionResult readStructFromHeap(final ExpressionResult old, final IL fieldIdentifiers.toArray(new String[fieldIdentifiers.size()]), fieldValues.toArray(new Expression[fieldValues.size()])); - final ExpressionResult result = new ExpressionResult(newStmt, new RValue(sc, structType), newDecl, newAuxVars, - old.getOverapprs(), old.getNeighbourUnionFields()); - return result; + return new ExpressionResult(newStmt, new RValue(sc, structType), newDecl, newAuxVars, old.getOverapprs(), + old.getNeighbourUnionFields()); } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResult.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResult.java index a6b8d753e76..49388067f1a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResult.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResult.java @@ -33,15 +33,13 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.BoogieASTNode; /** - * A Result for the C to Boogie translation. - * Stores the result of translating an initializer. - * An initializer essentially is a nested structure of ExpressionResults. + * A Result for the C to Boogie translation. Stores the result of translating an initializer. An initializer essentially + * is a nested structure of ExpressionResults. * * As a special case an initializer may contain only one ExpressionResult, for example for initializing simple type * variables, like ints. * - * This may also represent the translation of a struct initializer or of an initializer for a (multidimensional) - * array. + * This may also represent the translation of a struct initializer or of an initializer for a (multidimensional) array. * * This implementation tries to follow section 6.7.9 of the C11 standard. * @@ -52,21 +50,20 @@ public class InitializerResult extends Result { /** * Stores all the code that is needed for evaluating the initializer. * - * The values we store as RValues. - * So, if a switchToRValue introduced some Boogie code, it is saved in this top-level ExpressionResult. - * EDIT: because conversions work on ExpressionResults, we need to store ExpressionResults in the nodes (those can - * can always hold RValues, though). We will need some flattening or so to get all Boogie code from all the nodes. + * The values we store as RValues. So, if a switchToRValue introduced some Boogie code, it is saved in this + * top-level ExpressionResult. EDIT: because conversions work on ExpressionResults, we need to store + * ExpressionResults in the nodes (those can can always hold RValues, though). We will need some flattening or so to + * get all Boogie code from all the nodes. * * The RValue at the root of the tree is the RValue of this ExpressionResult. * - * (We can/could also use this class for - * initializers of non-aggregate type) + * (We can/could also use this class for initializers of non-aggregate type) */ private final ExpressionResult mRootExpressionResult; /** - * The RValue in mExpressionResult may have a designator. This field stores it. - * (Can happen only if we are inside a nested initializer.) + * The RValue in mExpressionResult may have a designator. This field stores it. (Can happen only if we are inside a + * nested initializer.) */ private final Designator mRootDesignator; @@ -74,7 +71,8 @@ public class InitializerResult extends Result { /** * - * @param node just for handing through to super class, can be null + * @param node + * just for handing through to super class, can be null * @param expressionResult * @param treeNodeIds * @param treeNodeIdToRValue @@ -146,7 +144,8 @@ public static ExpressionResult getFirstValueInInitializer(final InitializerResul throw new AssertionError("found no value in initializer"); } - public static abstract class Designator { } + public static abstract class Designator { + } public static class StructDesignator extends Designator { final String mStructFieldId; @@ -182,4 +181,3 @@ public String toString() { } } } - diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResultBuilder.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResultBuilder.java index 6443ecbc36c..67a9deadb28 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResultBuilder.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/InitializerResultBuilder.java @@ -63,12 +63,11 @@ public InitializerResultBuilder() { public InitializerResultBuilder(final InitializerResult initializerResult) { mRootDesignator = initializerResult.getRootDesignator(); - mRootExpressionResult = initializerResult.hasRootExpressionResult() ? - new ExpressionResultBuilder() - .addAllExceptLrValue(initializerResult.getRootExpressionResult()) - .setLrValue(initializerResult.getRootExpressionResult().getLrValue()) - .build() : - null; + mRootExpressionResult = + initializerResult.hasRootExpressionResult() + ? new ExpressionResultBuilder().addAllExceptLrValue(initializerResult.getRootExpressionResult()) + .setLrValue(initializerResult.getRootExpressionResult().getLrValue()).build() + : null; mChildren = initializerResult.isInitializerList() ? new ArrayList<>(initializerResult.getList()) : null; } @@ -91,7 +90,6 @@ public InitializerResultBuilder setRootDesignator(final String fieldDesignatorNa return this; } - public InitializerResultBuilder setRootDesignator(final Integer arrayDesignatorNumber) { if (mRootDesignator != null) { throw new IllegalStateException("cannot set root designator twice"); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java index 7909c5f9919..5c18958898d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java @@ -120,10 +120,10 @@ public boolean isNullPointerConstant() { if (value instanceof StructConstructor) { final StructConstructor sc = (StructConstructor) value; - if (sc.getFieldValues().length == 2 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) && - sc.getFieldIdentifiers()[1].equals(SFO.POINTER_OFFSET) && - BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])) && - BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1]))) { + if (sc.getFieldValues().length == 2 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) + && sc.getFieldIdentifiers()[1].equals(SFO.POINTER_OFFSET) + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])) + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1]))) { return true; } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/SkipResult.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/SkipResult.java index cef01eab897..98a209deb74 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/SkipResult.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/SkipResult.java @@ -3,27 +3,27 @@ * Copyright (C) 2015 Oleksii Saukh (saukho@informatik.uni-freiburg.de) * Copyright (C) 2015 Stefan Wissert * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ /** @@ -31,7 +31,6 @@ */ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result; - /** * @author Markus Lindenmann * @author Oleksii Saukh diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/TypesResult.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/TypesResult.java index 923e48c575c..04a20364045 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/TypesResult.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/TypesResult.java @@ -36,10 +36,8 @@ /** * Result that is returned whenever we dispatch a type specifier. * - * TODO 2018-10-22 Matthias: It seems that this kind of result is - * (sometimes) also returned when we dispatch a type declaration. - * I think this is not desired any more and happens only for - * historical reasons. + * TODO 2018-10-22 Matthias: It seems that this kind of result is (sometimes) also returned when we dispatch a type + * declaration. I think this is not desired any more and happens only for historical reasons. * * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de) * @author Markus Lindenmann diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/TarjanSCC.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/TarjanSCC.java index 20749370ddd..650478d01ab 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/TarjanSCC.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/TarjanSCC.java @@ -81,7 +81,7 @@ public final class TarjanSCC { * @return a list of SCCs */ public ImmutableSet> getSCCs(final Map> graph) { - if (graph == null || graph.values().contains(null)) { + if (graph == null || graph.containsValue(null)) { throw new IllegalArgumentException(); } mGraph = graph; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IACSLHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IACSLHandler.java index 8489f1274f4..115b4594570 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IACSLHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IACSLHandler.java @@ -4,31 +4,31 @@ * Copyright (C) 2015 Oleksii Saukh (saukho@informatik.uni-freiburg.de) * Copyright (C) 2015 Stefan Wissert * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ /** - * + * */ package de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler; @@ -67,171 +67,182 @@ public interface IACSLHandler extends IHandler { /** * Translates an CodeAnnot. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, CodeAnnot node); - + Result visit(IDispatcher main, CodeAnnot node); + /** * Translates an BinaryExpression. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, BinaryExpression node); - + Result visit(IDispatcher main, BinaryExpression node); + /** * Translates an UnaryExpression. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, UnaryExpression node); - + Result visit(IDispatcher main, UnaryExpression node); + /** * Translates an IntegerLiteral. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IntegerLiteral node); - + Result visit(IDispatcher main, IntegerLiteral node); + /** * Translates an BooleanLiteral. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, BooleanLiteral node); - + Result visit(IDispatcher main, BooleanLiteral node); + /** * Translates an RealLiteral. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, RealLiteral node); - + Result visit(IDispatcher main, RealLiteral node); + /** * Translates an IdentifierExpression. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IdentifierExpression node); - + Result visit(IDispatcher main, IdentifierExpression node); + /** * Translates an Contract. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, Contract node); - + Result visit(IDispatcher main, Contract node); + /** * Translates an Requires. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, Requires node); - + Result visit(IDispatcher main, Requires node); + /** * Translates an Ensures. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, Ensures node); - + Result visit(IDispatcher main, Ensures node); + /** * Translates an Assigns. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, Assigns node); - + Result visit(IDispatcher main, Assigns node); + /** * Translates an ResultExpression. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, ACSLResultExpression node); - + Result visit(IDispatcher main, ACSLResultExpression node); + /** * Translates an LoopAnnot. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, LoopAnnot node); - + Result visit(IDispatcher main, LoopAnnot node); + /** * Translates an LoopInvariant. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, LoopInvariant node); - + Result visit(IDispatcher main, LoopInvariant node); + /** * Translates an LoopVariant. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, LoopVariant node); - + Result visit(IDispatcher main, LoopVariant node); + /** * Translates an LoopAssigns. + * + * @param main + * a reference to the main IDispatcher + * @param node + * the node to visit + * @return a result object + */ + Result visit(IDispatcher main, LoopAssigns node); + + /** + * Translates an ArrayAccessExpression. * * @param main * a reference to the main IDispatcher @@ -239,66 +250,54 @@ public interface IACSLHandler extends IHandler { * the node to visit * @return a result object */ - public Result visit(IDispatcher main, LoopAssigns node); - + Result visit(IDispatcher main, ArrayAccessExpression node); + + /** + * Translates an FieldAccessExpression. + * + * @param main + * a reference to the main IDispatcher + * @param node + * the node to visit + * @return a result object + */ + Result visit(IDispatcher main, FieldAccessExpression node); + + /** + * Translates an FreeableExpression. + * + * @param main + * a reference to the main IDispatcher + * @param node + * the node to visit + * @return a result object + */ + Result visit(IDispatcher main, FreeableExpression node); + /** - * Translates an ArrayAccessExpression. - * - * @param main - * a reference to the main IDispatcher - * @param node - * the node to visit - * @return a result object - */ - public Result visit(IDispatcher main, ArrayAccessExpression node); - - /** - * Translates an FieldAccessExpression. - * - * @param main - * a reference to the main IDispatcher - * @param node - * the node to visit - * @return a result object - */ - public Result visit(IDispatcher main, FieldAccessExpression node); - - /** - * Translates an FreeableExpression. - * - * @param main - * a reference to the main IDispatcher - * @param node - * the node to visit - * @return a result object - */ - public Result visit(IDispatcher main, FreeableExpression node); - - /** - * Translates an MallocableExpression. - * - * @param main - * a reference to the main IDispatcher - * @param node - * the node to visit - * @return a result object - */ - public Result visit(IDispatcher main, MallocableExpression node); - - /** - * Translates an ValidExpression. - * - * @param main - * a reference to the main IDispatcher - * @param node - * the node to visit - * @return a result object - */ - public Result visit(IDispatcher main, ValidExpression node); - - public Result visit(IDispatcher main, CastExpression node); - - public Result visit(IDispatcher main, IfThenElseExpression node); - - + * Translates an MallocableExpression. + * + * @param main + * a reference to the main IDispatcher + * @param node + * the node to visit + * @return a result object + */ + Result visit(IDispatcher main, MallocableExpression node); + + /** + * Translates an ValidExpression. + * + * @param main + * a reference to the main IDispatcher + * @param node + * the node to visit + * @return a result object + */ + Result visit(IDispatcher main, ValidExpression node); + + Result visit(IDispatcher main, CastExpression node); + + Result visit(IDispatcher main, IfThenElseExpression node); + } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IHandler.java index d5974e10bbe..f0fb09dd444 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IHandler.java @@ -54,7 +54,7 @@ public interface IHandler { * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTNode node); + Result visit(IDispatcher main, IASTNode node); /** * Visit a given ACSL node. @@ -65,5 +65,5 @@ public interface IHandler { * the node to visit * @return a result object */ - public Result visit(IDispatcher main, ACSLNode node); + Result visit(IDispatcher main, ACSLNode node); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/INameHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/INameHandler.java index 0cb4920393a..c6da58b470f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/INameHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/INameHandler.java @@ -58,7 +58,7 @@ public interface INameHandler { * CType of the object for which we need an identifier * @return an unique identifier. */ - public String getUniqueIdentifier(IASTNode scope, String cId, int compCnt, boolean isOnHeap, CType cType, + String getUniqueIdentifier(IASTNode scope, String cId, int compCnt, boolean isOnHeap, CType cType, DeclarationInformation decInfo); /** @@ -79,11 +79,11 @@ public String getUniqueIdentifier(IASTNode scope, String cId, int compCnt, boole */ String getInParamIdentifier(String cid, CType cType, DeclarationInformation decInfo); - public String getGloballyUniqueIdentifier(String looplabel); + String getGloballyUniqueIdentifier(String looplabel); - public boolean isTempVar(String id); + boolean isTempVar(String id); - public String getTempVarUIDForBlockScope(AUXVAR auxVarType, CType cType); + String getTempVarUIDForBlockScope(AUXVAR auxVarType, CType cType); void addFunction(final String boogieId, final CType returnType); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IPreprocessorHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IPreprocessorHandler.java index 08ae52fd7ec..d09813fc70d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IPreprocessorHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/IPreprocessorHandler.java @@ -49,122 +49,122 @@ public interface IPreprocessorHandler extends IHandler { /** * Translates an IASTPreprocessorElifStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorElifStatement node); + Result visit(IDispatcher main, IASTPreprocessorElifStatement node); /** * Translates an IASTPreprocessorElseStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorElseStatement node); + Result visit(IDispatcher main, IASTPreprocessorElseStatement node); /** * Translates an IASTPreprocessorEndifStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorEndifStatement node); + Result visit(IDispatcher main, IASTPreprocessorEndifStatement node); /** * Translates an IASTPreprocessorErrorStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorErrorStatement node); + Result visit(IDispatcher main, IASTPreprocessorErrorStatement node); /** * Translates an IASTPreprocessorIfdefStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorIfdefStatement node); + Result visit(IDispatcher main, IASTPreprocessorIfdefStatement node); /** * Translates an IASTPreprocessorIfndefStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorIfndefStatement node); + Result visit(IDispatcher main, IASTPreprocessorIfndefStatement node); /** * Translates an IASTPreprocessorIfStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorIfStatement node); + Result visit(IDispatcher main, IASTPreprocessorIfStatement node); /** * Translates an IASTPreprocessorIncludeStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorIncludeStatement node); + Result visit(IDispatcher main, IASTPreprocessorIncludeStatement node); /** * Translates an IASTPreprocessorMacroDefinition. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorMacroDefinition node); + Result visit(IDispatcher main, IASTPreprocessorMacroDefinition node); /** * Translates an IASTPreprocessorPragmaStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorPragmaStatement node); + Result visit(IDispatcher main, IASTPreprocessorPragmaStatement node); /** * Translates an IASTPreprocessorUndefStatement. - * + * * @param main * a reference to the main IDispatcher * @param node * the node to visit * @return a result object */ - public Result visit(IDispatcher main, IASTPreprocessorUndefStatement node); + Result visit(IDispatcher main, IASTPreprocessorUndefStatement node); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/ACSLObjectContainerObserver.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/ACSLObjectContainerObserver.java index 58f76251397..15588ec5939 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/ACSLObjectContainerObserver.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/ACSLObjectContainerObserver.java @@ -1,22 +1,22 @@ /* * Copyright (C) 2016 Vincent Langenfeld (langenfv@informatik.uni-freiburg.de) * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE TraceAbstraction plug-in. - * + * * The ULTIMATE TraceAbstraction plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE TraceAbstraction plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE TraceAbstraction plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE TraceAbstraction plug-in, or any covered work, by linking * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Activator.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Activator.java index bc3f997db1d..77833844cbc 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Activator.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Activator.java @@ -4,27 +4,27 @@ * Copyright (C) 2015 Oleksii Saukh (saukho@informatik.uni-freiburg.de) * Copyright (C) 2015 Stefan Wissert * Copyright (C) 2015 University of Freiburg - * + * * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify * it under the terms of the GNU Lesser General Public License as published * by the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. - * + * * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Lesser General Public License for more details. - * + * * You should have received a copy of the GNU Lesser General Public License * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . - * + * * Additional permission under GNU GPL version 3 section 7: * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking - * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), - * containing parts covered by the terms of the Eclipse Public License, the - * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission * to convey the resulting work. */ /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java index 79f70d488bc..ef5a06d2f1d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java @@ -134,7 +134,7 @@ public BacktranslatedExpression translateEnsuresExpression( private Optional computeOldVarEqualities(final String proc, final Set modifiableGlobals) { - final var modifiableNames = modifiableGlobals.stream().map(e -> e.getIdentifier()).collect(Collectors.toSet()); + final var modifiableNames = modifiableGlobals.stream().map(de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression::getIdentifier).collect(Collectors.toSet()); final boolean modifiesMemory = modifiableNames.stream().anyMatch(name -> name.startsWith(SFO.MEMORY)); return mSymbolTable.getGlobalScope().entrySet().stream().flatMap( diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java index b7c731511d9..14a12c9642f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java @@ -84,6 +84,7 @@ import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.ConditionAnnotation; import de.uni_freiburg.informatik.ultimate.core.lib.results.GenericResult; import de.uni_freiburg.informatik.ultimate.core.lib.translation.DefaultTranslator; +import de.uni_freiburg.informatik.ultimate.core.lib.translation.DefaultTranslator.IFunction; import de.uni_freiburg.informatik.ultimate.core.lib.translation.ProgramExecutionFormatter; import de.uni_freiburg.informatik.ultimate.core.model.models.IExplicitEdgesMultigraph; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; @@ -420,8 +421,8 @@ private int handleCASTFunctionCallExpression(final IProgramExecution translateCFG(final IBacktransla // printCFG(cfg, mLogger::info); final boolean oldValue = mGenerateBacktranslationWarnings; mGenerateBacktranslationWarnings = false; - IBacktranslatedCFG translated = translateCFG(cfg, (a, b, c) -> translateCFGEdge(a, b, c), + IBacktranslatedCFG translated = translateCFG(cfg, (IFunction, Multigraph>, IMultigraphEdge, Multigraph, Multigraph>) this::translateCFGEdge, (a, b, c) -> new CACSLBacktranslatedCFG(a, b, c, mLogger, mServices)); translated = reduceCFGs(translated); // mLogger.info("################# Output: " + translated.getClass().getSimpleName()); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieTranslatorObserver.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieTranslatorObserver.java index 8408a96f422..ec56a9fae54 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieTranslatorObserver.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieTranslatorObserver.java @@ -89,7 +89,7 @@ public boolean process(final IElement root) { return false; } - if ((root instanceof WrapperNode) && (((WrapperNode) root).getBacking() instanceof ASTDecorator)) { + if (root instanceof WrapperNode && ((WrapperNode) root).getBacking() instanceof ASTDecorator) { mInputDecorator = (ASTDecorator) ((WrapperNode) root).getBacking(); if (mInputDecorator.countUnits() == 1) { final IASTTranslationUnit translationUnit = mInputDecorator.getUnit(0).getSourceTranslationUnit(); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/LTLExpressionExtractor.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/LTLExpressionExtractor.java index ca5c8506afa..f25ff5575e5 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/LTLExpressionExtractor.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/LTLExpressionExtractor.java @@ -95,13 +95,13 @@ public static String getAPSymbol(final int i) { return String.valueOf(ALPHABET.charAt(i)); } - String rtr = "A"; + StringBuilder rtr = new StringBuilder("A"); int idx = i; while (idx > ALPHABET.length()) { idx = idx - ALPHABET.length(); - rtr += String.valueOf(ALPHABET.charAt(idx % ALPHABET.length())); + rtr.append(ALPHABET.charAt(idx % ALPHABET.length())); } - return rtr; + return rtr.toString(); } private class LTLReplaceWeakUntil extends ACSLTransformer { @@ -152,7 +152,6 @@ private class LTLFormatStringPrinter extends LTLPrettyPrinter { */ public LTLFormatStringPrinter(final Set subExpressions, final Map apString2Expr) { - super(); mApString2Expr = apString2Expr; mSubExpressions = subExpressions; mAPCounter = 0; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java index 7d864590255..c89245e447d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java @@ -42,9 +42,10 @@ */ public class CACSLPreferenceInitializer extends UltimatePreferenceInitializer { - private static final String MAINPROC_DESC = - "Specify the entry function of the program. " + "Use an empty string for library mode " - + "(i.e., assume all globals are non-deterministic and verify each function in isolation)."; + private static final String MAINPROC_DESC = """ + Specify the entry function of the program. \ + Use an empty string for library mode \ + (i.e., assume all globals are non-deterministic and verify each function in isolation)."""; public static final String LABEL_ERROR = "Check unreachability of reach_error function"; private static final String DESC_ERROR = "Check if every call to reach_error is unreachable. This is used for the ReachSafety category of SV-COMP. " @@ -61,11 +62,12 @@ public class CACSLPreferenceInitializer extends UltimatePreferenceInitializer { public static final String LABEL_CHECK_MEMORY_LEAK_IN_MAIN = "Check for the main procedure if all allocated memory was freed"; public static final String LABEL_SVCOMP_MEMTRACK_COMPATIBILITY_MODE = "SV-COMP memtrack compatibility mode"; - public static final String DESC_SVCOMP_MEMTRACK_COMPATIBILITY_MODE = "Report UNKNOWN instead of UNSAFE if not all " - + "allocated memory was freed at the end of the main procedure. Rationale: at the SV-COMP we have to check " - + "if the program lost track of allocated memory. If this is set to false we are unsound (at SV-COMP) in " - + "cases where not all memory is freed but pointers to that memory are live at the end of the " - + "main procedure."; + public static final String DESC_SVCOMP_MEMTRACK_COMPATIBILITY_MODE = """ + Report UNKNOWN instead of UNSAFE if not all \ + allocated memory was freed at the end of the main procedure. Rationale: at the SV-COMP we have to check \ + if the program lost track of allocated memory. If this is set to false we are unsound (at SV-COMP) in \ + cases where not all memory is freed but pointers to that memory are live at the end of the \ + main procedure."""; public static final String LABEL_MEMORY_MODEL = "Memory model"; public static final String LABEL_POINTER_INTEGER_CONVERSION = "Pointer-integer casts"; public static final String LABEL_CHECK_ARRAYACCESSOFFHEAP = "Check array bounds for arrays that are off heap"; @@ -82,10 +84,10 @@ public class CACSLPreferenceInitializer extends UltimatePreferenceInitializer { public static final String LABEL_ASSUME_NONDET_VALUES_IN_RANGE = "Assume nondeterminstic values are in range"; public static final String LABEL_BITVECTOR_TRANSLATION = "Use bitvectors instead of ints"; public static final String LABEL_OVERAPPROXIMATE_FLOATS = "Overapproximate operations on floating types"; - private static final String DESC_OVERAPPROXIMATE_FLOATS = - "Overapproximate all operations on floats (including plus, minus, multiplication, conversions, etc.) by " - + "havoc. The resulting analysis will be fast and sound, but the result is UNKNOWN if such an " - + "operation occurs in a counterexample."; + private static final String DESC_OVERAPPROXIMATE_FLOATS = """ + Overapproximate all operations on floats (including plus, minus, multiplication, conversions, etc.) by \ + havoc. The resulting analysis will be fast and sound, but the result is UNKNOWN if such an \ + operation occurs in a counterexample."""; public static final String LABEL_FP_TO_IEEE_BV_EXTENSION = "Use Z3's non-standard fp.to_ieee_bv extension"; public static final String LABEL_FP_ROUNDING_MODE_INITIAL = "Initial rounding mode"; @@ -126,10 +128,11 @@ public class CACSLPreferenceInitializer extends UltimatePreferenceInitializer { public static final String LABEL_ADAPT_MEMORY_MODEL_ON_POINTER_CASTS = "Adapt memory model on pointer casts if necessary"; - public static final String DESC_ADAPT_MEMORY_MODEL_ON_POINTER_CASTS = "When a pointer to a value with a small type " - + "(e.g. char) is cast to a larger pointer type (e.g. int*), and the memory model resolution is larger than " - + "the values's pointed to type size (for char: 1 Byte), the memory model is unsound. When this setting is " - + "on we attempt to detect this case, and automatically set the memory model to a higher resolution."; + public static final String DESC_ADAPT_MEMORY_MODEL_ON_POINTER_CASTS = """ + When a pointer to a value with a small type \ + (e.g. char) is cast to a larger pointer type (e.g. int*), and the memory model resolution is larger than \ + the values's pointed to type size (for char: 1 Byte), the memory model is unsound. When this setting is \ + on we attempt to detect this case, and automatically set the memory model to a higher resolution."""; public static final String LABEL_STRING_OVERAPPROXIMATION_THRESHOLD = "String overapproximation threshold"; public static final String DESC_STRING_OVERAPPROXIMATION_THRESHOLD = "String literals that require this number of " diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java index e697de17b65..cd253186459 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/witness/GraphMLCorrectnessWitnessExtractor.java @@ -79,10 +79,10 @@ public class GraphMLCorrectnessWitnessExtractor extends CorrectnessWitnessExtrac public GraphMLCorrectnessWitnessExtractor(final IUltimateServiceProvider service) { super(service); - mLoopTypes = Arrays.asList(new Class[] { IASTGotoStatement.class, IASTDoStatement.class, - IASTWhileStatement.class, IASTForStatement.class }); - mConditionalTypes = Arrays.asList(new Class[] { IASTDoStatement.class, IASTWhileStatement.class, - IASTForStatement.class, IASTIfStatement.class }); + mLoopTypes = Arrays.asList(IASTGotoStatement.class, IASTDoStatement.class, IASTWhileStatement.class, + IASTForStatement.class); + mConditionalTypes = Arrays.asList(IASTDoStatement.class, IASTWhileStatement.class, IASTForStatement.class, + IASTIfStatement.class); mCheckOnlyLoopInvariants = mPrefs.getBoolean(WitnessParserPreferences.LABEL_CW_USE_ONLY_LOOPINVARIANTS); } @@ -217,8 +217,7 @@ private Map matchWitnessToAstNode(final WitnessNode } private Map matchWitnessToAstNode(final WitnessNode wnode) { - final Set edges = new HashSet<>(); - edges.addAll(convertAndFilterEdges(wnode.getIncomingEdges(), true)); + final Set edges = new HashSet<>(convertAndFilterEdges(wnode.getIncomingEdges(), true)); edges.addAll(convertAndFilterEdges(wnode.getOutgoingEdges(), false)); if (edges.isEmpty()) { @@ -242,7 +241,7 @@ private Map matchWitnessToAstNode(final WitnessNode } final Set outgoingEdges = getOutgoingSet(edges); - if (candidateNodes.stream().allMatch(a -> a.isIncoming()) && !outgoingEdges.isEmpty()) { + if (candidateNodes.stream().allMatch(MatchedASTNode::isIncoming) && !outgoingEdges.isEmpty()) { mLogger.warn( "Could not match AST node to invariant after witness lines " + toStringCollection(outgoingEdges)); printlabel = true; @@ -274,8 +273,7 @@ private Map extractInvariants(final DecoratedWitness candidateNodes.stream().forEach(a -> mLogger.warn(" " + a.toStringSimple())); return rtr; } - rtr = mergeMatchesIfNecessary(rtr, extractStatementInvariants(dwnode, candidateNodes)); - return rtr; + return mergeMatchesIfNecessary(rtr, extractStatementInvariants(dwnode, candidateNodes)); } private Map extractLoopInvariants(final DecoratedWitnessNode dwnode, @@ -286,7 +284,7 @@ private Map extractLoopInvariants(final DecoratedWit } else { // TODO 20221126 Matthias: This filter excludes all outgoing edges of a loop // head which makes it more difficult to find a match. - loopHeads = candidateNodes.stream().filter(a -> a.isLoopHead()).collect(Collectors.toSet()); + loopHeads = candidateNodes.stream().filter(MatchedASTNode::isLoopHead).collect(Collectors.toSet()); } candidateNodes.removeAll(loopHeads); @@ -349,7 +347,7 @@ private Map tryMatchLoopInvariantsUpwards(final Deco // check if the common parent or a parent of the common parent is a loop IASTNode currentParent = commonParent; Set loopStatements = Collections.emptySet(); - while (currentParent != null && currentParent instanceof IASTStatement) { + while (currentParent instanceof IASTStatement) { loopStatements = CdtASTUtils.findDesiredType(currentParent, mLoopTypes); if (!loopStatements.isEmpty()) { break; @@ -466,7 +464,7 @@ private static IASTNode findCommonParentStatement(final Collection Stream getIncomingStream(final Collection edges) { - return edges.stream().filter(a -> a.isIncoming()); + return edges.stream().filter(IHasIncoming::isIncoming); } private static Set getIncomingSet(final Collection edges) { @@ -482,8 +480,8 @@ private static Set getOutgoingSet(final Collection String.valueOf(a)).collect(Collectors.toList())); + return String.join(", ", stream.map(String::valueOf).collect(Collectors.toList())); } private final class LineMatchingVisitor extends ASTGenericVisitor { @@ -733,7 +731,6 @@ private static final class LabeledInvariant { private final ImmutableSet mLabels; public LabeledInvariant(final ExtractedWitnessInvariant invariant, final ImmutableSet labels) { - super(); mInvariant = invariant; mLabels = labels; }