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

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;

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) {
@@ -326,8 +325,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/ExplorativeNameVisitor.java

@@ -135,4 +135,4 @@ private String toString(final IType type) {
 		}
 		return type + " (" + type.getClass().getSimpleName() + ")";
 	}
-}
+}

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<String, FunctionDeclaration> 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;
 	}

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<String, IASTNode> 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);

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

@@ -94,4 +94,4 @@ public interface IDispatcher {
 	List<ACSLNode> getFunctionContractFromWitness(IASTNode node);
 
 	Set<IExtractedWitnessDeclaration> getWitnessDeclarations();
-}
+}

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

@@ -3,27 +3,27 @@
  * Copyright (C) 2015 Oleksii Saukh ([email protected])
  * 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 <http://www.gnu.org/licenses/>.
- * 
+ *
  * 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<ACSLNode> 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<ACSLNode> acsl, final IASTNode successorCNode) {
 		assert acsl != null;

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

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

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