Improve error handling for floats in unions

* We check for the correct setting (i.e., the memory model).
* We don't check for floats at the declaration of the union, but only at the write.
* Instead of crashing, we model it as an unsupported feature, i.e., we only report unknown if it can be reached.

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

@@ -485,14 +485,6 @@ public Result visit(final IDispatcher main, final IASTCompositeTypeSpecifier nod
 		if (node.getKey() == IASTCompositeTypeSpecifier.k_struct) {
 			isStructOrUnion = StructOrUnion.STRUCT;
 		} else if (node.getKey() == IASTCompositeTypeSpecifier.k_union) {
-			// Currently the translation of unions that contain floats is unsound in the integer translation
-			// Therefore we throw an exception, s.t. we can continue in the bitvector translation, where this is
-			// correctly handled.
-			if (!mTranslationSettings.isBitvectorTranslation()
-					&& fTypes.stream().anyMatch(x -> x.getUnderlyingType().isFloatingType())) {
-				throw new UnsupportedSyntaxException(loc,
-						"floats in unions are not supported in the integer translation.");
-			}
 			isStructOrUnion = StructOrUnion.UNION;
 		} else {
 			throw new UnsupportedOperationException();

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

@@ -2602,11 +2602,17 @@ 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()) {