Use the correct location to overapproximate unions with floats

The issue does not only occur at writes (ae94f3b), so we put the overapproximation at the declaration instead.

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

@@ -2252,11 +2252,21 @@ public Result visit(final IDispatcher main, final IASTSimpleDeclaration node) {
 			final CDeclaration cDec = declResult.getDeclaration();
 			cDec.setStorageClass(storageClass);
 
-			// are we in prerun mode?
-			// all unions should be on heap
-			if (mIsPrerun && CStructOrUnion.isUnion(cDec.getType().getUnderlyingType())
-					&& storageClass != CStorageClass.TYPEDEF) {
-				addToVariablesOnHeap(declarator.getName());
+			final CType type = cDec.getType().getUnderlyingType();
+			if (CStructOrUnion.isUnion(type) && storageClass != CStorageClass.TYPEDEF) {
+				// For the memory model HoenickeLindenmann_Original, unions in floats are not handled properly,
+				// therefore we overapproximate them instead to avoid any unsoundness.
+				if (mSettings.getMemoryModelPreference() == MemoryModel.HoenickeLindenmann_Original
+						&& Arrays.stream(((CStructOrUnion) type).getFieldTypes()).anyMatch(CType::isFloatingType)) {
+					final Statement stmt = ExpressionTranslation.modelUnsupportedFeature(loc,
+							"union with floats in the HoenickeLindenmann_Original memory model");
+					intermediateResults.add(new ExpressionResultBuilder().addStatement(stmt).build());
+				}
+				// are we in prerun mode?
+				// all unions should be on heap
+				if (mIsPrerun) {
+					addToVariablesOnHeap(declarator.getName());
+				}
 			}
 
 			if (cDec.getType() instanceof CFunction && storageClass != CStorageClass.TYPEDEF) {

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

@@ -2602,17 +2602,11 @@ private List<Statement> getWriteCallArray(final ILocation loc, final HeapLValue
 	private List<Statement> getWriteCallStruct(final ILocation loc, final HeapLValue hlv, final Expression value,
 			final CStructOrUnion valueType, final HeapWriteMode writeMode) {
 		final List<Statement> stmt = new ArrayList<>();
-		final boolean checkForFloats = CStructOrUnion.isUnion(valueType)
-				&& mSettings.getMemoryModelPreference() == MemoryModel.HoenickeLindenmann_Original;
 		for (final String fieldId : valueType.getFieldIds()) {
 			final Expression startAddress = hlv.getAddress();
 			final Expression newStartAddressBase = MemoryHandler.getPointerBaseAddress(startAddress, loc);
 			final Expression newStartAddressOffset = MemoryHandler.getPointerOffset(startAddress, loc);
 			final CType fieldType = valueType.getFieldType(fieldId);
-			if (checkForFloats && fieldType.getUnderlyingType().isFloatingType()) {
-				stmt.add(ExpressionTranslation.modelUnsupportedFeature(loc,
-						"write for union with floats in the HoenickeLindenmann_Original memory model"));
-			}
 			final StructAccessExpression sae = ExpressionFactory.constructStructAccessExpression(loc, value, fieldId);
 			final Offset fieldOffset = mTypeSizeAndOffsetComputer.constructOffsetForField(loc, valueType, fieldId);
 			if (fieldOffset.isBitfieldOffset()) {