From 860c6ccc941bf8669f9fde83b89e7cb19122f247 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frank=20Sch=C3=BCssele?=
 <schuessf@informatik.uni-freiburg.de>
Date: Wed, 27 Nov 2024 11:25:41 +0100
Subject: [PATCH] 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.

---
 .../implementation/base/CHandler.java         | 20 ++++++++++++++-----
 .../base/chandler/MemoryHandler.java          |  6 ------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java
index f9b0c3fc6ed..370fcfe7cc2 100644
--- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/CHandler.java
+++ b/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) {
diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java
index baf718fec75..a451e06a85a 100644
--- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java
+++ b/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()) {