Apply CC fixes to existing code

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/LineDirectiveMapping.java

@@ -40,7 +40,6 @@ public class LineDirectiveMapping {
 	private final TreeMap<Integer, Pair<Integer, String>> mMapping;
 
 	public LineDirectiveMapping(final String file) {
-		super();
 		mMapping = constructLineDirectiveMapping(file);
 	}
 
@@ -104,7 +103,7 @@ public Pair<Integer, String> 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());
 	}
 

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<IASTNode> nodes = new HashSet<>();
-				nodes.add(myNode);
-				nodes.add(otherNode);
-				return CdtASTUtils.findCommonParent(nodes);
-			}
+			final Collection<IASTNode> nodes = new HashSet<>();
+			nodes.add(myNode);
+			nodes.add(otherNode);
+			return CdtASTUtils.findCommonParent(nodes);
 		}
 	}
 

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/LocationFactory.java

@@ -119,7 +119,7 @@ public CACSLProjectLocation(final Set<IASTTranslationUnit> 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<String> getFilenames() {

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));

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 ([email protected])
  *
@@ -32,4 +32,4 @@ public Set<IdentifierExpression> getGlobalIdentifierExpressions(final Expression
 		super.processExpression(expr);
 		return Collections.unmodifiableSet(mResult);
 	}
-}
+}

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 ([email protected])
  *
@@ -34,4 +33,4 @@ public VariableLHS getGlobalId(final LeftHandSide lhs) {
 		super.processLeftHandSide(lhs);
 		return mResult;
 	}
-}
+}

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);
 	}
 
 	/**

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CTranslationUtil.java

@@ -160,8 +160,7 @@ public static List<Integer> getConstantDimensionsOfArray(final CArray cArrayType
 
 		final List<Integer> 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<Integer> 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];

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);
 				});
 	}

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;
 		}

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);
 		}

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() + ")";
 	}
-}
+}