Add workaround for misparsed casts

trunk/examples/programs/regression/c/castLibraryType.c

@@ -0,0 +1,15 @@
+//#Safe
+/* 
+ * Test where the parser misparses the cast to a function call (as the includes are ignored).
+ * 
+ * Author: [email protected]
+ * Date: 2025-12-15
+ * 
+ */
+
+#include <stdint.h>
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+  if ((size_t)(x) < 0) reach_error();
+}

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

@@ -1099,8 +1099,6 @@ public Result visit(final IDispatcher main, final IASTCaseStatement node) {
 	}
 
 	public Result visit(final IDispatcher main, final IASTCastExpression node) {
-		final ILocation loc = mLocationFactory.createCLocation(node);
-
 		// TODO: check validity of cast?
 
 		final TypesResult resTypes = (TypesResult) main.dispatch(node.getTypeId().getDeclSpecifier());
@@ -1111,24 +1109,30 @@ public Result visit(final IDispatcher main, final IASTCastExpression node) {
 		mCurrentDeclaredTypes.pop();
 
 		final ExpressionResult expr = (ExpressionResult) main.dispatch(node.getOperand());
-		ExpressionResult exprWithType = new ExpressionResultBuilder().addAllSideEffects(declResult)
-				.addAllExceptLrValue(expr).setLrValue(expr.getLrValue()).build();
+		final ExpressionResult exprWithType =
+				new ExpressionResultBuilder().addAllSideEffects(declResult).addAllIncludingLrValue(expr).build();
+		return handleCast(newCType, node, exprWithType);
+	}
 
-		if (!exprWithType.hasLRValue()) {
+	private Result handleCast(final ICType type, final IASTNode node, final ExpressionResult exprResult) {
+		final ILocation loc = mLocationFactory.createCLocation(node);
+		final ExpressionResult exprResultReady;
+		if (exprResult.hasLRValue()) {
+			exprResultReady = mExprResultTransformer.rexBoolToInt(
+					mExprResultTransformer.makeRepresentationReadyForConversion(exprResult, loc, type, node), loc);
+		} else {
 			// creates a void expression for null RValues
 			final Expression newExpression = ExpressionFactory.createVoidDummyExpression(loc);
 			final RValue rVal = new RValue(newExpression, new CPrimitive(CPrimitives.VOID));
-			exprWithType = new ExpressionResultBuilder().addAllExceptLrValue(exprWithType).setLrValue(rVal).build();
+			exprResultReady = new ExpressionResultBuilder(exprResult).setLrValue(rVal).build();
 		}
-		exprWithType = mExprResultTransformer.makeRepresentationReadyForConversion(exprWithType, loc, newCType, node);
-		checkUnsupportedPointerCast(exprWithType, loc, newCType);
+		checkUnsupportedPointerCast(exprResultReady, loc, type);
 
 		if (mSettings.isAdaptMemoryStructureResolutionOnPointerCasts() && mIsPrerun) {
-			checkIfNecessaryMemoryStructureAdaption(loc, newCType, exprWithType);
+			checkIfNecessaryMemoryStructureAdaption(loc, type, exprResultReady);
 		}
 
-		exprWithType = mExprResultTransformer.rexBoolToInt(exprWithType, loc);
-		return mExprResultTransformer.performImplicitConversion(exprWithType, newCType, loc);
+		return mExprResultTransformer.performImplicitConversion(exprResultReady, type, loc);
 	}
 
 	private void checkIfNecessaryMemoryStructureAdaption(final ILocation loc, final ICType castTargetType,
@@ -1727,6 +1731,13 @@ public Result visit(final IDispatcher main, final IASTFunctionCallExpression nod
 				throw new UnsupportedSyntaxException(loc, "Thread local variables are not supported yet.");
 			}
 		}
+		// WOKAROUND: On non-preprocessed files, casts may be accidentally misparsed as function calls, if the type is
+		// defined in some include (e.g., size_t) that we currently don't handle, if the expression is also in
+		// parentheses. In that case we just handle the handle the "function call" in the AST just as a cast.
+		final ICType castType = getTypeOfMisparsedCast(node);
+		if (castType != null) {
+			return handleCast(castType, node, (ExpressionResult) main.dispatch(node.getArguments()[0]));
+		}
 		final Result standardFunction = mLibraryModelHandler.translateStandardFunction(main, node);
 		if (standardFunction != null) {
 			return standardFunction;
@@ -1735,6 +1746,16 @@ public Result visit(final IDispatcher main, final IASTFunctionCallExpression nod
 				mMemoryHandler);
 	}
 
+	private ICType getTypeOfMisparsedCast(final IASTFunctionCallExpression node) {
+		if (node.getArguments().length == 1
+				&& node.getFunctionNameExpression() instanceof final IASTUnaryExpression unary
+				&& unary.getOperator() == IASTUnaryExpression.op_bracketedPrimary
+				&& unary.getOperand() instanceof final IASTIdExpression id) {
+			return mTypeHandler.getLibraryType(id.getName().toString());
+		}
+		return null;
+	}
+
 	public Result visit(final IDispatcher main, final IASTFunctionDefinition node) {
 		if (!isReachable(node)) {
 			// Unreachable function declaration. Test for parent=TU skipped: Not necessary,

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

@@ -858,6 +858,11 @@ public void addLibraryTypes(final Map<String, ICType> libraryTypes) {
 		mLibraryTypes.putAll(libraryTypes);
 	}
 
+	@Override
+	public ICType getLibraryType(final String name) {
+		return mLibraryTypes.get(name);
+	}
+
 	public static boolean isCharArray(final ICType cTypeRaw) {
 		return cTypeRaw.getUnderlyingType() instanceof final CArray cArrayType
 				&& cArrayType.getValueType().getUnderlyingType() instanceof final CPrimitive cPrimitive

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java

@@ -190,5 +190,7 @@ public interface ITypeHandler {
 
 	void addLibraryTypes(Map<String, ICType> libraryTypes);
 
+	ICType getLibraryType(String name);
+
 	IMemoryPointer getMemoryPointer();
 }