From 0c8cc6c4027f38376fc097e699ae93c12ea57f62 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 19:51:32 +0100 Subject: [PATCH 01/20] remove unused "unchecked read procedures" Unchecked reads are done directly as array accesses (as documented for MemoryHandler::getReadUnchecked) hence there do not exist corresponding procedures. --- .../base/chandler/IMemoryStructure.java | 4 ---- .../implementation/base/chandler/MemoryModel.java | 8 -------- .../base/chandler/MemoryStructureBase.java | 11 ----------- 3 files changed, 23 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java index 1292c1c13f0..14a3cb38ba3 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java @@ -40,8 +40,6 @@ public interface IMemoryStructure { String getReadProcedureName(final CPrimitives primitive); - String getUncheckedReadProcedureName(final CPrimitives primitive); - String getWriteProcedureName(final CPrimitives primitive); String getUncheckedWriteProcedureName(final CPrimitives primitive); @@ -50,8 +48,6 @@ public interface IMemoryStructure { String getReadPointerProcedureName(); - String getUncheckedReadPointerProcedureName(); - String getWritePointerProcedureName(); String getUncheckedWritePointerProcedureName(); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 16332fae28d..8c7a7d0c55a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -79,10 +79,6 @@ public String getReadProcedureName(final CPrimitives primitive) { return mMemoryStructure.getReadProcedureName(primitive); } - public String getUncheckedReadProcedureName(final CPrimitives primitive) { - return mMemoryStructure.getUncheckedReadProcedureName(primitive); - } - public String getWriteProcedureName(final CPrimitives primitive) { return mMemoryStructure.getWriteProcedureName(primitive); } @@ -99,10 +95,6 @@ public String getReadPointerProcedureName() { return mMemoryStructure.getReadPointerProcedureName(); } - public String getUncheckedReadPointerProcedureName() { - return mMemoryStructure.getUncheckedReadPointerProcedureName(); - } - public String getWritePointerProcedureName() { return mMemoryStructure.getWritePointerProcedureName(); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java index 79d209e6079..1bdb38d89e8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java @@ -74,11 +74,6 @@ public final String getReadProcedureName(final CPrimitives primitive) { return READ_PROCEDURE_PREFIX + getProcedureSuffix(primitive); } - @Override - public final String getUncheckedReadProcedureName(final CPrimitives primitive) { - return READ_PROCEDURE_PREFIX + UNCHECKED_PREFIX + getProcedureSuffix(primitive); - } - @Override public final String getWriteProcedureName(final CPrimitives primitive) { return WRITE_PROCEDURE_PREFIX + getProcedureSuffix(primitive); @@ -100,12 +95,6 @@ public final String getReadPointerProcedureName() { return READ_PROCEDURE_PREFIX + hda.getName(); } - @Override - public final String getUncheckedReadPointerProcedureName() { - final HeapDataArray hda = mPointerArray; - return READ_PROCEDURE_PREFIX + UNCHECKED_PREFIX + hda.getName(); - } - @Override public final String getWritePointerProcedureName() { final HeapDataArray hda = mPointerArray; From 82cc759cfedf91280d3dea8e20d1c91f22eeb756 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 20:04:19 +0100 Subject: [PATCH 02/20] MemoryHandler::getReadUnchecked is guaranteed to return only an expression Hence, there is no need to wrap it into an ExpressionResult. --- .../base/chandler/MemoryHandler.java | 7 +++---- .../base/chandler/StructHandler.java | 12 ++++++++---- .../ConstructMemcpyOrMemmove.java | 18 ++---------------- .../result/ExpressionResultTransformer.java | 17 +++++++++++------ 4 files changed, 24 insertions(+), 30 deletions(-) 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 a82d9d54f19..702fde05328 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 @@ -663,9 +663,9 @@ public ExpressionResult getReadCall(final Expression address, final ICType resul * the address to read from. * @param resultType * the CType of the pointer - * @return an ExpressionResult consisting only of a array access to the memory array. + * @return an array access to the memory array. */ - public ExpressionResult getReadUnchecked(final Expression address, final ICType resultType) { + public Expression getReadUnchecked(final Expression address, final ICType resultType) { final int byteSize; if (resultType instanceof CPointer) { byteSize = mTypeSizes.getSizeOfPointer(); @@ -675,8 +675,7 @@ public ExpressionResult getReadUnchecked(final Expression address, final ICType throw new AssertionError("We only support reading primitive or pointer types"); } final ILocation loc = address.getLocation(); - return new ExpressionResult(new RValue( - readFromHeap(loc, determineMemoryArrayForType(resultType), address, resultType, byteSize), resultType)); + return readFromHeap(loc, determineMemoryArrayForType(resultType), address, resultType, byteSize); } private String determineReadProcedure(final ICType resultType, final ILocation loc) throws AssertionError { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java index 7b463cd0098..f360417b7e4 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java @@ -217,11 +217,15 @@ public Result readFieldInTheStructAtAddress(final ILocation loc, final int field final ICType resultType = structType.getFieldTypes()[fieldIndex]; - final ExpressionResult call = unchecked ? mMemoryHandler.getReadUnchecked(newPointer, resultType) - : mMemoryHandler.getReadCall(newPointer, resultType); final ExpressionResultBuilder resultBuilder = new ExpressionResultBuilder(); - resultBuilder.addAllExceptLrValue(call); - resultBuilder.setLrValue(new RValue(call.getLrValue().getValue(), resultType)); + if (unchecked) { + final Expression read = mMemoryHandler.getReadUnchecked(newPointer, resultType); + resultBuilder.setLrValue(new RValue(read, resultType)); + } else { + final ExpressionResult call = mMemoryHandler.getReadCall(newPointer, resultType); + resultBuilder.addAllExceptLrValue(call); + resultBuilder.setLrValue(new RValue(call.getLrValue().getValue(), resultType)); + } return resultBuilder.build(); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java index da572fa975f..596f6e84e91 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java @@ -244,14 +244,7 @@ destId, new RValue(loopCtrAux.getExp(), mExpressionTranslation.getCTypeOfPointer for (final CPrimitives cPrim : mMemoryHandler.getRequiredMemoryStructureFeatures() .getDataOnHeapRequired()) { final ICType cPrimType = new CPrimitive(cPrim); - final Expression srcAcc; - { - final ExpressionResult srcAccExpRes = mMemoryHandler.getReadUnchecked(currentSrc, cPrimType); - srcAcc = srcAccExpRes.getLrValue().getValue(); - loopBody.addStatements(srcAccExpRes.getStatements()); - loopBody.addDeclarations(srcAccExpRes.getDeclarations()); - assert srcAccExpRes.getOverapprs().isEmpty(); - } + final Expression srcAcc = mMemoryHandler.getReadUnchecked(currentSrc, cPrimType); { final List writeCall = mMemoryHandler.getWriteCall(ignoreLoc, @@ -293,14 +286,7 @@ destId, new RValue(loopCtrAux.getExp(), mExpressionTranslation.getCTypeOfPointer if (mMemoryHandler.getRequiredMemoryStructureFeatures().isPointerOnHeapRequired()) { final ICType cPointer = CPointer.voidPointer(); - final Expression srcAcc; - { - final ExpressionResult srcAccExpRes = mMemoryHandler.getReadUnchecked(currentSrc, cPointer); - srcAcc = srcAccExpRes.getLrValue().getValue(); - loopBody.addStatements(srcAccExpRes.getStatements()); - loopBody.addDeclarations(srcAccExpRes.getDeclarations()); - assert srcAccExpRes.getOverapprs().isEmpty(); - } + final Expression srcAcc = mMemoryHandler.getReadUnchecked(currentSrc, cPointer); { final List writeCall = mMemoryHandler.getWriteCall(ignoreLoc, diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java index c82a15ac87e..582de331add 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java @@ -264,9 +264,7 @@ private ExpressionResult switchToRValue(final ExpressionResult expr, final ILoca final ExpressionResultBuilder erb = new ExpressionResultBuilder().addAllExceptLrValue(expr); final RValue newValue; if (underlyingType instanceof CPrimitive || underlyingType instanceof CPointer) { - final ExpressionResult rex = - unchecked ? mMemoryHandler.getReadUnchecked(hlv.getAddress(), underlyingType) - : mMemoryHandler.getReadCall(hlv.getAddress(), underlyingType); + final ExpressionResult rex = readAsExpressionResult(hlv.getAddress(), unchecked, underlyingType); newValue = (RValue) rex.getLrValue(); erb.addAllExceptLrValue(rex); } else if (underlyingType instanceof final CArray cArray) { @@ -466,10 +464,8 @@ private ExpressionResult readArrayFromHeap(final ExpressionResult old, final ILo final ExpressionResult readRex; if (arrayValueType instanceof final CStructOrUnion cStructOrUnion) { readRex = readStructFromHeap(old, loc, addressExpr, cStructOrUnion, hook, unchecked); - } else if (unchecked) { - readRex = mMemoryHandler.getReadUnchecked(addressExpr, arrayType.getValueType()); } else { - readRex = mMemoryHandler.getReadCall(addressExpr, arrayType.getValueType()); + readRex = readAsExpressionResult(addressExpr, unchecked, arrayType.getValueType()); } builder.addAllExceptLrValue(readRex); builder.setOrResetLrValue(readRex.getLrValue()); @@ -487,6 +483,15 @@ private ExpressionResult readArrayFromHeap(final ExpressionResult old, final ILo return builder.build(); } + private ExpressionResult readAsExpressionResult(final Expression addressExpr, final boolean unchecked, + final ICType resultType) { + if (unchecked) { + final Expression read = mMemoryHandler.getReadUnchecked(addressExpr, resultType); + return new ExpressionResult(new RValue(read, resultType)); + } + return mMemoryHandler.getReadCall(addressExpr, resultType); + } + /** * Convert Expression of some type to an expression of boolean type. If the expression expr *
    From 99b123949bbd744341bfea79f30f232f784a7380 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 20:05:51 +0100 Subject: [PATCH 03/20] MemoryStructureMultiBitprecise: exhaustive switch --- .../chandler/MemoryStructureMultiBitprecise.java | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java index 5a315821897..032c7920a72 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java @@ -59,16 +59,11 @@ public MemoryStructureMultiBitprecise(final TypeSizes typeSizes, final ITypeHand @Override public HeapDataArray getDataHeapArray(final CPrimitives primitive) { - switch (primitive.getPrimitiveCategory()) { - case FLOATTYPE: - return getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapFloatingArray); - case INTTYPE: - return getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapIntegerArray); - case VOID: - throw new AssertionError("void on the heap???"); - default: - throw new AssertionError("unknown primitive category"); - } + return switch (primitive.getPrimitiveCategory()) { + case FLOATTYPE -> getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapFloatingArray); + case INTTYPE -> getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapIntegerArray); + case VOID -> throw new AssertionError("void on the heap???"); + }; } private HeapDataArray getDataHeapArrayForGivenGeneralType(final CPrimitives primitive, From 7fddee1ee278d4bf336f9811afdbb54f15c653c8 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 20:19:12 +0100 Subject: [PATCH 04/20] IMemoryPointer::isNullPointer: avoid throwing ClassCastExceptions Perform instanceof-check inside the method for safe casting, instead of leaving it to the caller. Simplify the implementations and the calling code. --- .../implementation/base/chandler/MemoryHandler.java | 6 ++---- .../implementation/base/chandler/MemoryPointer1D.java | 10 +++------- .../implementation/base/chandler/MemoryPointer2D.java | 10 +++------- .../cdt/translation/implementation/result/LRValue.java | 6 +----- 4 files changed, 9 insertions(+), 23 deletions(-) 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 702fde05328..3a85ed0d6a4 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 @@ -77,7 +77,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.StructAccessExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.StructConstructor; import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VarList; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableDeclaration; @@ -907,9 +906,8 @@ public void requireMemoryModelFeature(final MemoryModelDeclarations mmDecl) { * caution or improve this method. */ public boolean isNullPointerLiteral(final Expression expr) { - - if (expr instanceof StructConstructor) { - return mMemoryPointer.isNullPointer(expr); + if (mMemoryPointer.isNullPointer(expr)) { + return true; } final BigInteger integerValue = mTypeSizes.extractIntegerValue(expr, new CPrimitive(CPrimitives.LONG)); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java index 560cd745864..9106e36a221 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java @@ -167,12 +167,8 @@ public Expression constructPointerComponentRelation(final ILocation loc, final i @Override public boolean isNullPointer(final Expression ptr) { - final StructConstructor sc = (StructConstructor) ptr; - if (sc.getFieldValues().length == 1 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) - && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0]))) { - return true; - } - - return false; + return ptr instanceof final StructConstructor sc && sc.getFieldValues().length == 1 + && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java index bbe6fb2d3d3..b0ae623adca 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java @@ -167,14 +167,10 @@ public Expression constructPointerComponentRelation(final ILocation loc, final i @Override public boolean isNullPointer(final Expression ptr) { - final StructConstructor sc = (StructConstructor) ptr; - if (sc.getFieldValues().length == 2 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) + return ptr instanceof final StructConstructor sc && sc.getFieldValues().length == 2 + && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) && sc.getFieldIdentifiers()[1].equals(SFO.POINTER_OFFSET) && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])) - && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1]))) { - return true; - } - - return false; + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1])); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java index 70499cac6a0..ee7d9d9cd6d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java @@ -30,7 +30,6 @@ import java.math.BigInteger; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.StructConstructor; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CTranslationUtil; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; @@ -118,9 +117,6 @@ public boolean isNullPointerConstant(final IMemoryPointer memoryPointer) { return true; } - if (value instanceof StructConstructor) { - return memoryPointer.isNullPointer(value); - } - return false; + return memoryPointer.isNullPointer(value); } } From 7fcd3ad3eced4c78c9212f4dfce361757f6d595f Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 20:20:33 +0100 Subject: [PATCH 05/20] IMemoryPointer::constructPointerRelationExpression: exhaustive switches --- .../base/chandler/MemoryPointer1D.java | 13 ++++--------- .../base/chandler/MemoryPointer2D.java | 17 ++++++----------- 2 files changed, 10 insertions(+), 20 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java index 9106e36a221..e5d45d359bc 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java @@ -147,15 +147,10 @@ public Expression constructPointerRelationExpression(final ILocation loc, final final Expression pointerRelation = constructPointerComponentRelation(loc, op, left.getLrValue().getValue(), right.getLrValue().getValue(), SFO.POINTER_BASE, expressionTranslation); - switch (mPointerSubtractionAndComparisonValidityCheckMode) { - case CHECK: - case ASSUME: - return ExpressionFactory.createBooleanLiteral(loc, true); - case IGNORE: - return pointerRelation; - default: - throw new AssertionError("unknown value"); - } + return switch (mPointerSubtractionAndComparisonValidityCheckMode) { + case CHECK, ASSUME -> ExpressionFactory.createBooleanLiteral(loc, true); + case IGNORE -> pointerRelation; + }; } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java index b0ae623adca..5efd3d13018 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java @@ -144,18 +144,13 @@ public Expression constructPointerRelationExpression(final ILocation loc, final final Expression offsetRelation = constructPointerComponentRelation(loc, op, left.getLrValue().getValue(), right.getLrValue().getValue(), SFO.POINTER_OFFSET, expressionTranslation); - switch (mPointerSubtractionAndComparisonValidityCheckMode) { - case CHECK: - case ASSUME: - return offsetRelation; - case IGNORE: - // use conjunction - return ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, baseEquality, offsetRelation); - // TODO: Do not use conjunction. Use nondeterministic value if baseEquality does not hold. - default: - throw new AssertionError("unknown value"); - } + return switch (mPointerSubtractionAndComparisonValidityCheckMode) { + case CHECK, ASSUME -> offsetRelation; + // use conjunction + // TODO: Do not use conjunction. Use nondeterministic value if baseEquality does not hold. + case IGNORE -> ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, baseEquality, offsetRelation); + }; } @Override From 06100560caf6414547688633c138bf3d2cb02337 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 20:25:02 +0100 Subject: [PATCH 06/20] use pattern-matching instead of casts --- .../base/chandler/MemoryPointer2D.java | 4 ++-- .../implementation/base/chandler/TypeSizes.java | 8 ++++---- .../translation/implementation/result/LRValue.java | 12 ++++++------ 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java index 5efd3d13018..aede32205db 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java @@ -118,8 +118,8 @@ public Expression constructInitialPointer(final ILocation loc, final BigInteger * @return The offset. */ public Expression pointerOffset(final Expression pointer, final ILocation loc) { - if (pointer instanceof StructConstructor) { - return ((StructConstructor) pointer).getFieldValues()[1]; + if (pointer instanceof final StructConstructor sc) { + return sc.getFieldValues()[1]; } return ExpressionFactory.constructStructAccessExpression(loc, pointer, SFO.POINTER_OFFSET); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java index 3f831278718..0088684b91b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java @@ -282,8 +282,8 @@ public BigInteger extractIntegerValue(final RValue rval) { } public BigInteger extractIntegerValue(final Expression expr, final ICType cType) { - if (expr instanceof IntegerLiteral) { - final BigInteger value = new BigInteger(((IntegerLiteral) expr).getValue()); + if (expr instanceof final IntegerLiteral intLit) { + final BigInteger value = new BigInteger(intLit.getValue()); final CPrimitive cPrimitive = (CPrimitive) CEnum.replaceEnumWithInt(cType); if (!isUnsigned(cPrimitive)) { return value; @@ -294,8 +294,8 @@ public BigInteger extractIntegerValue(final Expression expr, final ICType cType) final BigInteger maxValuePlusOne = maxValue.add(BigInteger.ONE); return value.mod(maxValuePlusOne); } - if (expr instanceof BitvecLiteral) { - final BigInteger value = new BigInteger(((BitvecLiteral) expr).getValue()); + if (expr instanceof final BitvecLiteral bvLit) { + final BigInteger value = new BigInteger(bvLit.getValue()); final CPrimitive cPrimitive = (CPrimitive) CEnum.replaceEnumWithInt(cType); if (isUnsigned(cPrimitive)) { if (getMinValueOfPrimitiveType(cPrimitive).compareTo(value) > 0) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java index ee7d9d9cd6d..949651f52c8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java @@ -83,10 +83,10 @@ public boolean isIntFromPointer() { @Override public final String toString() { - if (this instanceof HeapLValue) { - return "address: " + ((HeapLValue) this).getAddress(); - } else if (this instanceof LocalLValue) { - return "lhs: " + ((LocalLValue) this).getLhs(); + if (this instanceof final HeapLValue hlv) { + return "address: " + hlv.getAddress(); + } else if (this instanceof final LocalLValue llv) { + return "lhs: " + llv.getLhs(); } else { return "value: " + getValue(); } @@ -106,8 +106,8 @@ public boolean isNullPointerConstant(final IMemoryPointer memoryPointer) { } final Expression value; - if (this instanceof HeapLValue) { - value = ((HeapLValue) this).getAddress(); + if (this instanceof final HeapLValue hlv) { + value = hlv.getAddress(); throw new AssertionError("unexpected: double check this case"); } value = getValue(); From 3d15c5b39a4dea75ed4c21849e4126855df68a98 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 21:05:36 +0100 Subject: [PATCH 07/20] move handling of specifications out of IMemoryAddressing The appropriate accounting for CheckMode, the correct Spec, etc. should not have to be implemented anew for every addressing mode. --- .../base/chandler/IMemoryAdressing.java | 16 +---- .../base/chandler/MemoryAddressing1D.java | 8 --- .../base/chandler/MemoryAddressing2D.java | 54 ++------------- .../base/chandler/MemoryAdressingBase.java | 20 ++---- .../base/chandler/MemoryHandler.java | 65 +++++++++++++++---- .../base/chandler/MemoryModel.java | 26 ++------ 6 files changed, 70 insertions(+), 119 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index ae457a033fb..d4ff7a9f02f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -35,7 +35,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; @@ -139,16 +138,6 @@ Expression constructAddressForStructField(final ILocation loc, final Expression Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant); - /** - * Constructs the specifications that the pointer base address is valid. - * - * @return The specifications. - */ - List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** * Constructs the pointer base validity check expression. * @@ -163,9 +152,8 @@ Expression constructPointerValidityCheckExpr(final ILocation loc, final Expressi * * @return The specifications. */ - List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, Expression ptr, final Expression size, + final boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java index 658caefdf55..f20f799b168 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java @@ -208,14 +208,6 @@ public List constructReallocBodyStatements(final ILocation loc, final return stmts; } - @Override - public Expression constructPointerValidityCheckExpr(final ILocation loc, final Expression ptr, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - throw new UnsupportedOperationException("The pointer validity check is not available with the 1D Addressing"); - - } - @Override public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index 1f801319401..e290f640315 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -37,8 +37,6 @@ import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; -import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; -import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation.StorageClass; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.StatementFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayAccessExpression; @@ -46,11 +44,8 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.RequiresSpecification; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; @@ -141,44 +136,12 @@ public Expression addIntegerConstantToPointer(final ILocation loc, final Express } @Override - public List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - final Expression ptrExpr = - ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, - new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); - final Expression isValid = constructPointerValidityCheckExpr(loc, ptrExpr, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - - final boolean isFreeRequires = mode == CheckMode.CHECK ? false : true; - - final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, isValid); - final Check check = new Check(Spec.MEMORY_DEREFERENCE); - check.annotate(spec); - return Collections.singletonList(spec); - } - - @Override - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - final Expression ptrExpr = - ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, - new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); - - final Expression ptrBase = mMemoryPointer.getPointerAddress(ptrExpr, loc); - final Expression ptrOffset = mMemoryPointer.pointerOffset(ptrExpr, loc); + final Expression ptrBase = mMemoryPointer.getPointerAddress(ptr, loc); + final Expression ptrOffset = mMemoryPointer.pointerOffset(ptr, loc); final CPrimitive cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); final Expression lengthArray = MemoryMetadataDefault2D.getLengthArray(loc, requiredMemoryModelFeatures, @@ -206,14 +169,7 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca leq = ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, noOverFlowInSum); } - final Expression offsetInAllocatedRange = - ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, offsetGeqZero); - - final boolean isFreeRequires = mode == CheckMode.CHECK ? false : true; - final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, offsetInAllocatedRange); - final Check check = new Check(Spec.MEMORY_DEREFERENCE); - check.annotate(spec); - return Collections.singletonList(spec); + return ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, offsetGeqZero); } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index 81c8f8755ad..1311122a43b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -36,7 +36,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; @@ -210,30 +209,21 @@ public Expression[] constructRhsAssignmentStatementHda(final ILocation loc, fina } @Override - public List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, + public Expression constructPointerValidityCheckExpr(final ILocation loc, final Expression ptr, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException("The pointer base validity check is not compatible with the selected: " + this.getClass() + " addressing mode!"); } @Override - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException( "The target pointer fully allocated check is not compatible with the selected: " + this.getClass() - + " " + "addressing mode!"); + + " addressing mode!"); } @Override 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 3a85ed0d6a4..aa860e2c0c7 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 @@ -74,6 +74,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.NamedAttribute; import de.uni_freiburg.informatik.ultimate.boogie.ast.Procedure; import de.uni_freiburg.informatik.ultimate.boogie.ast.QuantifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.RequiresSpecification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.StructAccessExpression; @@ -120,8 +121,11 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.INameHandler; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Overapprox; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Spec; +import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.MemoryStructure; import de.uni_freiburg.informatik.ultimate.util.datastructures.LinkedScopedHashMap; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; @@ -1751,13 +1755,13 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p * memory at the base address of the pointer. Furthermore, we check that the offset is greater than or equal to * zero. * - * In case mPointerBaseValidity is CHECK, we construct the requires specification + * In case {@code mSettings.checkPointerDerefValidity()} is CHECK, we construct the requires specification * requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). * - * In case mPointerBaseValidity is CHECK, we construct the free requires specification - * free requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). + * In case {@code mSettings.checkPointerDerefValidity()} is ASSUME, we construct the free requires + * specification free requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). * - * In case mPointerBaseValidity is IGNORE, we construct nothing. + * In case {@code mSettings.checkPointerDerefValidity()} is IGNORE, we construct nothing. * * @param loc * location of translation unit @@ -1769,17 +1773,36 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p */ public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, final String ptrName, final String procedureName) { - return mMemoryModel.constructPointerTargetFullyAllocatedCheck(loc, size, ptrName, procedureName, - mSettings.checkPointerDerefValidity(), mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } + + final Expression ptrExpr = + ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, + new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); + + final Expression offsetInAllocatedRange = mMemoryModel.constructPointerTargetFullyAllocatedCheckExpr(loc, + ptrExpr, size, mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + + final boolean isFreeRequires = mode == CheckMode.ASSUME; + final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, offsetInAllocatedRange); + final Check check = new Check(Spec.MEMORY_DEREFERENCE); + check.annotate(spec); + return Collections.singletonList(spec); } /** - * Construct specification that the pointer base address is valid. In case - * {@link #getPointerBaseValidityCheckMode()} is ASSERTandASSUME, we add the requires specification - * requires #valid[#ptr!base]. In case {@link #getPointerBaseValidityCheckMode()} is ASSERTandASSUME, - * we add the free requires specification free requires #valid[#ptr!base]. In case - * {@link #getPointerBaseValidityCheckMode()} is IGNORE, we add nothing. + * Construct specification that the pointer base address is valid. + * + * In case {@code mSettings.checkPointerDerefValidity()} is CHECK, we add the requires specification + * requires #valid[#ptr!base]. + * + * In case {@code mSettings.checkPointerDerefValidity()} is ASSUME, we add the free requires specification + * free requires #valid[#ptr!base]. + * + * In case {@code mSettings.checkPointerDerefValidity()} is IGNORE, we add nothing. * * @param loc * location of translation unit @@ -1791,8 +1814,24 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca */ public List constructPointerBaseValidityCheck(final ILocation loc, final String ptrName, final String procedureName) { - return mMemoryModel.constructPointerBaseValidityCheck(loc, ptrName, procedureName, - mSettings.checkPointerDerefValidity(), mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } + + final Expression ptrExpr = + ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, + new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); + + final Expression isValid = mMemoryModel.constructPointerBaseValidityCheckExpr(loc, ptrExpr, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + + final boolean isFreeRequires = mode == CheckMode.ASSUME; + + final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, isValid); + final Check check = new Check(Spec.MEMORY_DEREFERENCE); + check.annotate(spec); + return Collections.singletonList(spec); } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 8c7a7d0c55a..6ff75d07915 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -35,7 +35,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; @@ -237,25 +236,12 @@ public Expression addIntegerConstantToPointer(final ILocation loc, final Express return mMemoryAddressing.addIntegerConstantToPointer(loc, ptrExpr, integerConstant); } - /** - * Constructs the specifications that the pointer base address is valid. - * - * @return The specifications. - */ - public List constructPointerBaseValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructPointerValidityCheck(loc, ptrName, procedureName, mode, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); - } - /** * Constructs the pointer base validity check expression. * * @return The expression. */ - Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expression ptr, + public Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expression ptr, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { return mMemoryAddressing.constructPointerValidityCheckExpr(loc, ptr, requiredMemoryModelFeatures, @@ -267,12 +253,12 @@ Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expr * * @return The specifications. */ - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructPointerTargetFullyAllocatedCheck(loc, size, ptrName, procedureName, mode, - isBitVectorTranslation, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.constructPointerTargetFullyAllocatedCheckExpr(loc, ptr, size, isBitVectorTranslation, + requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** From 2809bae028450f32ca0942b4933720066bc9e617 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Tue, 9 Dec 2025 21:05:48 +0100 Subject: [PATCH 08/20] exhaustive switch --- .../implementation/base/chandler/MemoryAdressingBase.java | 3 --- 1 file changed, 3 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index 1311122a43b..b6778eb5d67 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -113,9 +113,6 @@ yield new OverapproximationUF2D(exprTranslation, functionDeclarations, typeHandl } else { throw new UnsupportedOperationException("Unknown pointer type " + mMemoryPointer.getClass()); } - default: - throw new UnsupportedOperationException( - "Pointer-Integer conversion not yet implemented " + pointerIntegerMode); }; } From 09ad6baff5091a225a9c0765e725ba060518c3bd Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Wed, 10 Dec 2025 10:55:04 +0100 Subject: [PATCH 09/20] remove ITypeHandler::getMemoryPointer() method It is not clear why this method should be part of this interface, and the only usage of this method was on a concrete implementation anyway. --- .../cdt/translation/implementation/base/TypeHandler.java | 1 - .../cdt/translation/interfaces/handler/ITypeHandler.java | 3 --- 2 files changed, 4 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java index d75df8a3831..7d8a2c95bf2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java @@ -865,7 +865,6 @@ public static boolean isCharArray(final ICType cTypeRaw) { || cPrimitive.getType() == CPrimitives.SCHAR); } - @Override public IMemoryPointer getMemoryPointer() { return mMemoryPointer; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java index cd99b1f7980..1a32f2beb54 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java @@ -50,7 +50,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.FlatSymbolTable; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.IDispatcher; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitiveCategory; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; @@ -189,6 +188,4 @@ public interface ITypeHandler { void registerNamedIncompleteType(String incompleteType, String named); void addLibraryTypes(Map libraryTypes); - - IMemoryPointer getMemoryPointer(); } From c9b75114616bee8db8e262b4d497838bc5a2d18a Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Wed, 10 Dec 2025 10:55:45 +0100 Subject: [PATCH 10/20] make class private again --- .../implementation/base/chandler/TypeSizeAndOffsetComputer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java index e8d8493d615..07c9c25470c 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java @@ -447,7 +447,7 @@ private interface SizeTValue { Expression asExpression(ILocation loc); } - class SizeTValueInteger implements SizeTValue { + private class SizeTValueInteger implements SizeTValue { private final BigInteger mValue; public SizeTValueInteger(final BigInteger value) { From 9767f71a9336ece199871efe74723f2a36479377 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Wed, 10 Dec 2025 10:56:15 +0100 Subject: [PATCH 11/20] exhaustive switch --- .../base/chandler/MemoryStructureFactory.java | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java index d19d62295f6..f977ba3317e 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java @@ -52,19 +52,17 @@ public static IMemoryStructure createMemoryStructure(final TranslationSettings s + " is only available in using the bitprecise translation"); } - switch (memoryStructurePreference) { + return switch (memoryStructurePreference) { case HoenickeLindenmann_1ByteResolution: case HoenickeLindenmann_2ByteResolution: case HoenickeLindenmann_4ByteResolution: case HoenickeLindenmann_8ByteResolution: - return new MemoryStructureSingleBitprecise(memoryStructurePreference.getByteSize(), typeSizes, typeHandler); + yield new MemoryStructureSingleBitprecise(memoryStructurePreference.getByteSize(), typeSizes, typeHandler); case HoenickeLindenmann_Original: if (settings.isBitvectorTranslation()) { - return new MemoryStructureMultiBitprecise(typeSizes, typeHandler); + yield new MemoryStructureMultiBitprecise(typeSizes, typeHandler); } - return new MemoryStructureUnbounded(typeSizes, typeHandler); - default: - throw new UnsupportedOperationException(memoryStructurePreference + " is an invalid memory structure."); - } + yield new MemoryStructureUnbounded(typeSizes, typeHandler); + }; } } From eb716533ef9638fc6fd19732ab8b34e64bf19400 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 12:09:50 +0100 Subject: [PATCH 12/20] SFO: remove unused MEMSET, MEMCPY fields --- .../ultimate/cdt/translation/implementation/util/SFO.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java index 43da8260023..26cab160172 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java @@ -179,13 +179,11 @@ public final class SFO { public static final String MEMCPY_DEST = "dest"; public static final String MEMCPY_SRC = "src"; public static final String MEMCPY_SIZE = "size"; - public static final String MEMCPY = "#memcpy"; public static final String STRCPY_DEST = "dest"; public static final String STRCPY_SRC = "src"; public static final String TO_INT = "#to_int"; - public static final String MEMSET = "ULTIMATE.memset"; /** * used for detecting data races From 819339ddb469140eb6a023e8fd8db22fc72975e5 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 12:42:35 +0100 Subject: [PATCH 13/20] Move creation of AssertStatements out of IMemoryAddressing::getChecksForFreeCall The appropriate accounting for settings, the correct Spec, etc. should not have to be implemented anew for every addressing mode. --- .../base/chandler/IMemoryAdressing.java | 4 +-- .../base/chandler/MemoryAddressing2D.java | 31 ++++++------------- .../base/chandler/MemoryAdressingBase.java | 8 ++--- .../base/chandler/MemoryHandler.java | 18 +++++++++-- .../base/chandler/MemoryModel.java | 8 ++--- 5 files changed, 34 insertions(+), 35 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index d4ff7a9f02f..62d637fd712 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -161,8 +161,8 @@ Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, Ex * * @return The statements. */ - List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index e290f640315..c126ce4d3e2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -32,7 +32,6 @@ import java.math.BigInteger; import java.util.ArrayList; import java.util.Collection; -import java.util.Collections; import java.util.List; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; @@ -202,15 +201,11 @@ private Expression constructPointerBinaryComparisonExpression(final ILocation lo } @Override - public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { assert pointerToBeFreed.getCType().getUnderlyingType() instanceof CPointer; - if (!isPointerCheckRequired) { - return Collections.emptyList(); - } - final var cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); final Expression zeroNumericExpr = @@ -225,7 +220,7 @@ public List getChecksForFreeCall(final ILocation loc, final RValue po final Expression addrBase = mMemoryPointer.getPointerAddress(pointerToBeFreed.getValue(), loc); final Expression[] idcFree = { addrBase }; - final List result = new ArrayList<>(); + final List result = new ArrayList<>(); /* * creating the specification according to C99:7.20.3.2-2: The free function causes the space pointed to by ptr @@ -234,32 +229,27 @@ public List getChecksForFreeCall(final ILocation loc, final RValue po * realloc function, or if the space has been deallocated by a call to free or realloc, the behavior is * undefined. */ - final Check check = new Check(Spec.MEMORY_FREE); - // assert (~addr!offset == 0); - final AssertStatement offsetZero = new AssertStatement(loc, - ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrOffset, zeroNumericExpr)); - check.annotate(offsetZero); + // ~addr!offset == 0; + final Expression offsetZero = + ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrOffset, zeroNumericExpr); result.add(offsetZero); // assert (~addr!base < #StackHeapBarrier); final Expression inHeapArea = mExpressionTranslation.constructBinaryComparisonIntegerExpression(loc, IASTBinaryExpression.op_lessThan, addrBase, cTypeOfPointerComponent, stackHeapBarrier, cTypeOfPointerComponent); - final AssertStatement assertInHeapArea = new AssertStatement(loc, inHeapArea); - check.annotate(assertInHeapArea); - result.add(assertInHeapArea); + result.add(inHeapArea); // ~addr!base == 0 final Expression isNullPtr = ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrBase, zeroNumericExpr); - // requires ~addr!base == 0 || #valid[~addr!base]; + // ~addr!base == 0 || #valid[~addr!base]; final Expression addrIsValid = mBooleanArrayHelper .compareWithTrue(ExpressionFactory.constructNestedArrayAccessExpression(loc, valid, idcFree)); - final AssertStatement baseValid = new AssertStatement(loc, - ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, isNullPtr, addrIsValid)); - check.annotate(baseValid); + final Expression baseValid = + ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, isNullPtr, addrIsValid); result.add(baseValid); return result; @@ -280,7 +270,6 @@ public Expression constructFunctionPointer(final ILocation loc, final BigInteger mTypeSizeAndOffsetComputer.getSizeT(), integerExpr, mTypeSizeAndOffsetComputer.getSizeT()); return mMemoryPointer.constructPointerFromBaseAndOffset(baseExpr, offsetMinus, loc); - } @Override diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index b6778eb5d67..b57fdce9fa9 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -224,15 +224,11 @@ public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation } @Override - public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { assert pointerToBeFreed.getCType().getUnderlyingType() instanceof CPointer; - if (!isPointerCheckRequired) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException( "The check if the freed pointer is valid is not compatible with the selected: " + this.getClass() + " addressing mode!"); 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 aa860e2c0c7..0f0702106b9 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 @@ -55,6 +55,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayLHS; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayType; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssertStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement; @@ -531,9 +532,22 @@ public VariableLHS getMemoryRaceArrayLhs(final ILocation loc) { mMemoryModelDeclarationsHandler); } - public Collection getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed) { - return mMemoryModel.getChecksForFreeCall(loc, pointerToBeFreed, mSettings.checkIfFreedPointerIsValid(), + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed) { + if (!mSettings.checkIfFreedPointerIsValid()) { + return Collections.emptyList(); + } + + final List checkExpressions = mMemoryModel.getChecksForFreeCall(loc, pointerToBeFreed, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + final List statements = + checkExpressions.stream(). map(expr -> new AssertStatement(loc, expr)).toList(); + + final Check check = new Check(Spec.MEMORY_FREE); + for (final Statement stmt : statements) { + check.annotate(stmt); + } + + return statements; } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 6ff75d07915..08e8a5a2926 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -266,11 +266,11 @@ public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation * * @return The statements. */ - List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.getChecksForFreeCall(loc, pointerToBeFreed, isPointerCheckRequired, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.getChecksForFreeCall(loc, pointerToBeFreed, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } /** From 6f17b0795ddd3a268263f8821b813b49b0df91a6 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 13:21:43 +0100 Subject: [PATCH 14/20] remove redundant method IMemoryAddressing::constructMemSafeStatementsForPointerExpression The logic implemented in this method was essentially the same as in the two already existing methods ::constructPointerValidityCheckExpr and ::constructPointerTargetFullyAllocatedCheckExpr. There is a slight edge case where the functionality differs: the old code checked "offset < length", whereas the new code (in ::constructPointerTargetFullyAllocatedCheckExpr) checks only "offset <= length". However, I suspect this difference is unintentional (I have added a TODO to clarify the correct behaviour). --- .../base/chandler/IMemoryAdressing.java | 11 ---- .../base/chandler/MemoryAddressing2D.java | 62 +------------------ .../base/chandler/MemoryAdressingBase.java | 15 ----- .../base/chandler/MemoryHandler.java | 35 +++++++++-- .../base/chandler/MemoryModel.java | 14 ----- 5 files changed, 32 insertions(+), 105 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index 62d637fd712..776ce4a66c2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -45,7 +45,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; @@ -211,16 +210,6 @@ AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expres final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** - * Constructs assert / assume statements for ptr memsafety checks. - * - * @return The statements. - */ - List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** * Construct the assume to check that src and dest don't overlap. * diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index c126ce4d3e2..8dc93714720 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -56,10 +56,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; -import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Spec; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.PointerIntegerConversion; /** @@ -149,6 +146,7 @@ public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation ExpressionFactory.constructNestedArrayAccessExpression(loc, lengthArray, new Expression[] { ptrBase }); final Expression sum = constructPointerBinaryArithmeticExpression(loc, IASTBinaryExpression.op_plus, size, ptrOffset); + // TODO 2026-01-01: Should this be IASTBinaryExpression.op_lessThan ? Expression leq = constructPointerBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessEqual, sum, aae); final Expression zeroNumericLiteral = @@ -348,64 +346,6 @@ public Expression constructInitialPointerFromPointer(final ILocation loc, final return mMemoryPointer.constructPointerFromBaseAndOffset(mMemoryPointer.getPointerAddress(ptr, loc), zero, loc); } - @Override - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - final List result = new ArrayList<>(); - - if (pointerBaseValid != CheckMode.IGNORE) { - - // valid[s.base] - final Expression validBase = constructPointerValidityCheckExpr(loc, ptr, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - final var stmt = statementDependentOnCheck(loc, pointerBaseValid, validBase); - result.add(stmt); - } - - if (pointerTargetFullyAllocated != CheckMode.IGNORE) { - // s.offset < length[s.base]) - final Expression ptrOffset = mMemoryPointer.pointerOffset(ptr, loc); - final Expression ptrBase = mMemoryPointer.getPointerAddress(ptr, loc); - - final Expression lengthArray = MemoryMetadataDefault2D.getLengthArray(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - - final Expression aae = ExpressionFactory.constructNestedArrayAccessExpression(loc, lengthArray, - new Expression[] { ptrBase }); - - final Expression offsetSmallerLength = - constructPointerBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessThan, ptrOffset, aae); - - // s.offset >= 0; - final var zeroExpr = mTypeSizes.constructLiteralForIntegerType(loc, - mExpressionTranslation.getCTypeOfPointerComponents(), BigInteger.ZERO); - - final Expression offsetNonnegative = constructPointerBinaryComparisonExpression(loc, - IASTBinaryExpression.op_greaterEqual, ptrOffset, zeroExpr); - - final Expression aAndB = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, offsetSmallerLength, - offsetNonnegative); - - final var stmt = statementDependentOnCheck(loc, pointerTargetFullyAllocated, aAndB); - result.add(stmt); - } - return result; - } - - private static Statement statementDependentOnCheck(final ILocation loc, final CheckMode check, - final Expression expr) { - if (check == CheckMode.CHECK) { - final AssertStatement assertion = new AssertStatement(loc, expr); - final Check chk = new Check(Spec.MEMORY_DEREFERENCE); - chk.annotate(assertion); - return assertion; - } - assert check == CheckMode.ASSUME : "missed a case?"; - return new AssumeStatement(loc, expr); - } - @Override public Statement checksForStringCopyOverlapping(final ILocation loc, final Expression src, final Expression srcId, final Expression destId, final Expression dest) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index b57fdce9fa9..abf3af6f4bb 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -27,7 +27,6 @@ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; import java.math.BigInteger; -import java.util.Collections; import java.util.List; import java.util.Set; @@ -53,7 +52,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.PointerIntegerConversion; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; @@ -234,19 +232,6 @@ public List getChecksForFreeCall(final ILocation loc, final RValue p + " addressing mode!"); } - @Override - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (pointerBaseValid == CheckMode.IGNORE && pointerTargetFullyAllocated == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - throw new UnsupportedOperationException( - "The MemSafety checks are not compatible with the selected: " + this.getClass() + " addressing mode!"); - } - @Override public Statement checksForStringCopyOverlapping(final ILocation loc, final Expression src, final Expression srcId, final Expression destId, final Expression dest) { 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 0f0702106b9..7acf2cc7988 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 @@ -2664,14 +2664,41 @@ private Attribute[] constructExpandAndSmtDefinedAttributesForSubArraySelect(fina /** * Construct assert statements that do memsafety checks for {@link pointerValue} if the corresponding settings are - * active. settings concerned are: - "Pointer base address is valid at dereference" - "Pointer to allocated memory - * at dereference" + * active. */ public List constructMemsafetyChecksForPointerExpression(final ILocation loc, final Expression pointerValue) { - return mMemoryModel.constructMemSafeStatementsForPointerExpression(loc, pointerValue, - mSettings.checkPointerDerefValidity(), mSettings.checkPointerDerefValidity(), + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } + + final List result = new ArrayList<>(); + + final Expression validBase = mMemoryModel.constructPointerBaseValidityCheckExpr(loc, pointerValue, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + result.add(statementDependentOnCheck(loc, mode, validBase)); + + final Expression zero = mExpressionTranslation.constructLiteralForIntegerType(loc, + mExpressionTranslation.getCTypeOfPointerComponents(), BigInteger.ZERO); + final Expression pointerTargetFullyAllocated = mMemoryModel.constructPointerTargetFullyAllocatedCheckExpr(loc, + pointerValue, zero, mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, + mMemoryModelDeclarationsHandler); + result.add(statementDependentOnCheck(loc, mode, pointerTargetFullyAllocated)); + + return result; + } + + private static Statement statementDependentOnCheck(final ILocation loc, final CheckMode check, + final Expression expr) { + if (check == CheckMode.CHECK) { + final AssertStatement assertion = new AssertStatement(loc, expr); + final Check chk = new Check(Spec.MEMORY_DEREFERENCE); + chk.annotate(assertion); + return assertion; + } + assert check == CheckMode.ASSUME : "missed a case?"; + return new AssumeStatement(loc, expr); } public List ultimateInitStatements(final ILocation loc) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 08e8a5a2926..9affef084d5 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -47,7 +47,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; @@ -343,19 +342,6 @@ public final AssumeStatement strChrAssumeStatement(final ILocation loc, final Ex requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } - /** - * Constructs assert / assume statements for ptr memsafety checks. - * - * @return The statements. - */ - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructMemSafeStatementsForPointerExpression(loc, ptr, pointerBaseValid, - pointerTargetFullyAllocated, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); - } - /** * Construct the assume to check that src and dest don't overlap. * From 180a8e394d4e276b208425e442606841a197a3ea Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 13:46:54 +0100 Subject: [PATCH 15/20] replace IMemoryAddressing::getValidArray with ::constructMemoryNeutralityCheckExpr The old method was only used for this purpose, but did not make sense for all memory models. Hence, this is now handled analogously to the methods for pointer validity checks. --- .../implementation/base/chandler/IMemoryAdressing.java | 7 ++++++- .../base/chandler/MemoryAddressing1D.java | 8 -------- .../base/chandler/MemoryAddressing2D.java | 9 +++++++-- .../base/chandler/MemoryAdressingBase.java | 8 ++++++++ .../implementation/base/chandler/MemoryHandler.java | 10 +++++----- .../implementation/base/chandler/MemoryModel.java | 6 ++++-- .../implementation/base/chandler/ProcedureManager.java | 10 +++------- 7 files changed, 33 insertions(+), 25 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index 776ce4a66c2..9c328dd1d7e 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -253,6 +253,11 @@ List constructReallocBodyStatements(final ILocation loc, final String final RequiredMemoryModelFeatures requiredFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + /** + * Constructs a boolean expression that, when evaluated at the end of a procedure invocation, results in + * {@code true} iff no memory is allocated that was not already allocated at the beginning of the invocation. + */ + Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java index f20f799b168..31c57ead537 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java @@ -207,12 +207,4 @@ public List constructReallocBodyStatements(final ILocation loc, final return stmts; } - - @Override - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - throw new UnsupportedOperationException( - "The valid array is not part of the metadata values from the 1D Addressing"); - - } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index 8dc93714720..ea8421a7ded 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -46,6 +46,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; @@ -415,8 +416,12 @@ public Expression constructPointerValidityCheckExpr(final ILocation loc, final E } @Override - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return MemoryMetadataDefault2D.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + final Expression validArray = + MemoryMetadataDefault2D.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, validArray, + ExpressionFactory.constructUnaryExpression(loc, UnaryExpression.Operator.OLD, validArray)); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index abf3af6f4bb..ec935e58a82 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -240,6 +240,14 @@ public Statement checksForStringCopyOverlapping(final ILocation loc, final Expre + " addressing mode!"); } + @Override + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + throw new UnsupportedOperationException("The check for memory neutrality is not compatible with the selected: " + + this.getClass() + " addressing mode!"); + } + /** * Creates a valid expression representing a pointer subtractions of a pointer component. The component is either * base or offset. 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 7acf2cc7988..4202917a85e 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 @@ -512,12 +512,12 @@ public static AssignmentStatement constructOneDimensionalArrayUpdate(final ILoca } /** - * @param loc - * location of translation unit - * @return new IdentifierExpression that represents the #valid array + * Constructs a boolean expression that, when evaluated at the end of a procedure invocation, results in + * {@code true} iff no memory is allocated that was not already allocated at the beginning of the invocation. */ - public Expression getValidArray(final ILocation loc) { - return mMemoryModel.getValidArray(loc, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc) { + return mMemoryModel.constructMemoryNeutralityCheckExpr(loc, mRequiredMemoryModelFeatures, + mMemoryModelDeclarationsHandler); } public Expression getMemoryRaceArray(final ILocation loc) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 9affef084d5..f0d273ee877 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -388,9 +388,11 @@ public List constructReallocBodyStatements(final ILocation loc, final memoryModelDeclarationsHandler); } - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.constructMemoryNeutralityCheckExpr(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java index 3c0997209ab..613a3d4b716 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java @@ -44,9 +44,7 @@ import java.util.stream.Collectors; import de.uni_freiburg.informatik.ultimate.boogie.BoogieVisitor; -import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; import de.uni_freiburg.informatik.ultimate.boogie.ast.Body; import de.uni_freiburg.informatik.ultimate.boogie.ast.CallStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; @@ -58,7 +56,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Procedure; import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableDeclaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.CACSLLocation; @@ -220,14 +217,13 @@ public List computeFinalProcedureDeclarations(final MemoryHandler m // model is required. Maybe we can require the memory model if the list of functions for which we // check memory neutrality is not empty. - final Expression vIe = memoryHandler.getValidArray(loc); + final Expression neutrality = memoryHandler.constructMemoryNeutralityCheckExpr(loc); + final int nrSpec = newSpec.length; final Check check = new Check(Spec.MEMORY_NEUTRAL); final ILocation ensLoc = LocationFactory.createLocation(loc); newSpecWithExtraEnsuresClauses = Arrays.copyOf(newSpec, nrSpec + 1); - newSpecWithExtraEnsuresClauses[nrSpec] = new EnsuresSpecification(ensLoc, false, - ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, vIe, - ExpressionFactory.constructUnaryExpression(loc, UnaryExpression.Operator.OLD, vIe))); + newSpecWithExtraEnsuresClauses[nrSpec] = new EnsuresSpecification(ensLoc, false, neutrality); check.annotate(newSpecWithExtraEnsuresClauses[nrSpec]); if (mSettings.isSvcompMemtrackCompatibilityMode()) { new Overapprox(Collections.singletonMap("memtrack", ensLoc)) From fee39142b42c0a38c7bf80ca09ae5bdb1bf1001e Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 14:16:03 +0100 Subject: [PATCH 16/20] Remove IMemoryAddressing::getLastCharOfString This method was overly specific and can easily be implemented by the single caller, using existing methods. Furthermore, the implementation in MemoryAddressing1D was incorrect: it simply returned "len-1" as a pointer. --- .../base/chandler/IMemoryAdressing.java | 8 -------- .../base/chandler/MemoryAddressing1D.java | 10 ---------- .../base/chandler/MemoryAddressing2D.java | 11 ----------- .../implementation/base/chandler/MemoryHandler.java | 5 ----- .../implementation/base/chandler/MemoryModel.java | 10 ---------- .../base/library/FunctionModelHelper.java | 13 ++++++++++--- 6 files changed, 10 insertions(+), 47 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index 9c328dd1d7e..a9f003b74c7 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -192,14 +192,6 @@ List getChecksForFreeCall(final ILocation loc, final RValue pointerT */ Expression addExpressionToPointer(final ILocation loc, final Expression ptrExpr, final Expression expr); - /** - * Returns a pointer to the last character of a string. - * - * @return The pointer. - */ - Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue); - /** * Creates the assume statement used in the handling of strchr. * diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java index 31c57ead537..725dfab48f1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java @@ -146,16 +146,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryPointer.createPointerFromBase(basePlus, loc); } - @Override - public Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, - IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len), sizeT, - mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); - - return mMemoryPointer.createPointerFromBase(lenMinusOne, loc); - } - @Override public AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expression tmpExpr, final Expression argSPtr, final Expression nullPtrExpr, diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index ea8421a7ded..54d797f5ad5 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -283,17 +283,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryPointer.constructPointerFromBaseAndOffset(base, offsetPlus, loc); } - @Override - public Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, - IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len), sizeT, - mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); - - return mMemoryPointer.constructPointerFromBaseAndOffset(mMemoryPointer.getPointerAddress(returnValue, loc), - lenMinusOne, loc); - } - @Override public AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expression tmpExpr, final Expression argSPtr, final Expression nullPtrExpr, 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 4202917a85e..19a068493b4 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 @@ -2720,11 +2720,6 @@ public final Expression createFunctionPointer(final ILocation loc, final BigInte return mMemoryModel.createFunctionPointer(loc, offset); } - public final Expression lastCharOfString(final ILocation loc, final CPrimitive sizeT, - final IdentifierExpression len, final IdentifierExpression returnValue) { - return mMemoryModel.lastCharOfString(loc, sizeT, len, returnValue); - } - public final Expression initialPointerFromPointer(final ILocation loc, final Expression ptr) { return mMemoryModel.initialPointerFromPointer(loc, ptr); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index f0d273ee877..f1ddba57dfb 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -310,16 +310,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryAddressing.addExpressionToPointer(loc, ptrExpr, expr); } - /** - * Returns a pointer to the last character of a string. - * - * @return The pointer. - */ - public Expression lastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - return mMemoryAddressing.getLastCharOfString(loc, sizeT, len, returnValue); - } - /** * Returns a pointer with the same base address but an offset of 0. * diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java index 00ac7b94e2e..6efbc9fbb4f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java @@ -342,10 +342,17 @@ public ExpressionResult getNondetStringOrNull(final ILocation loc) { body.add(mMemoryHandler.getUltimateMemAllocCall(len.getExp(), retvar.getLhs(), loc, MemoryArea.HEAP)); final var nullChar = mTypeSizes.constructLiteralForIntegerType(loc, charType, BigInteger.ZERO); - final var lastChar = mMemoryHandler.lastCharOfString(loc, sizeT, len.getExp(), retvar.getExp()); - body.addAll(mMemoryHandler.getWriteCall(loc, - LRValueFactory.constructHeapLValue(mTypeHandler, lastChar, charType, null), nullChar, charType, false)); + // *(retvar + (len - 1)) = '\0'; + { + final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, + IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len.getExp()), + sizeT, mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); + final Expression lastChar = mMemoryHandler.addExpressionToPointer(loc, retvar.getExp(), lenMinusOne); + body.addAll(mMemoryHandler.getWriteCall(loc, + LRValueFactory.constructHeapLValue(mTypeHandler, lastChar, charType, null), nullChar, charType, + false)); + } final var stmt = StatementFactory.constructIfStatement(loc, new WildcardExpression(loc), new Statement[] { setPtrToNull }, body.toArray(Statement[]::new)); From 5eed0e598c2a55729b56d2f742d6c2d29172ab61 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Thu, 1 Jan 2026 15:40:24 +0100 Subject: [PATCH 17/20] replace IMemoryAdressing::constructAddressForStructField by ::addExpressionToPointer --- .../base/chandler/IMemoryAdressing.java | 9 --------- .../base/chandler/InitializationHandler.java | 4 ++-- .../base/chandler/MemoryAddressing1D.java | 12 ------------ .../base/chandler/MemoryAddressing2D.java | 14 -------------- .../base/chandler/MemoryHandler.java | 10 ++++++---- .../implementation/base/chandler/MemoryModel.java | 14 -------------- .../base/chandler/StructHandler.java | 10 ++++------ .../result/ExpressionResultTransformer.java | 4 ++-- 8 files changed, 14 insertions(+), 63 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index a9f003b74c7..2c835cae6ab 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -38,7 +38,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; @@ -121,14 +120,6 @@ Expression doPointerArithmetic(final int operator, final ILocation loc, final Ex */ BigInteger getFixedAddressCounterCountingStep(final Expression size); - /** - * Returns the address for a field in a struct. - * - * @return The address. - */ - Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT); - /** * Adds an integer to a pointer. * diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java index 5329fecd005..e3080454170 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java @@ -1089,8 +1089,8 @@ public HeapLValue constructAddressForStructField(final ILocation loc, final Heap final CStructOrUnion cStructType = (CStructOrUnion) baseAddress.getCType().getUnderlyingType(); final var fieldOffset = mTypeSetAndOffsetComputer.constructOffsetForField(loc, cStructType, fieldIndex); - final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, baseAddress.getAddress(), - fieldOffset, mTypeSetAndOffsetComputer.getSizeT()); + final Expression newPointer = + mMemoryHandler.constructAddressForStructField(loc, baseAddress.getAddress(), fieldOffset); return LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, cStructType.getFieldTypes()[fieldIndex], null); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java index 725dfab48f1..441d2742b78 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java @@ -45,7 +45,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.TranslationSettings; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; 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; @@ -100,17 +99,6 @@ public BigInteger getFixedAddressCounterCountingStep(final Expression size) { return mTypeSizes.extractIntegerValue(size, new CPrimitive(CPrimitives.LONG)); } - @Override - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - - final Expression pointerBase = mMemoryPointer.getPointerAddress(baseAddress, loc); - final Expression sum = mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, - pointerBase, sizeT, fieldOffset.getAddressOffsetAsExpression(loc), sizeT); - - return mMemoryPointer.createPointerFromBase(sum, loc); - } - @Override public Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index 54d797f5ad5..9c38e4f09e1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -50,7 +50,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; @@ -109,19 +108,6 @@ public BigInteger getFixedAddressCounterCountingStep(final Expression size) { return BigInteger.ONE; } - @Override - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - - final Expression pointerBase = mMemoryPointer.getPointerAddress(baseAddress, loc); - final Expression pointerOffset = mMemoryPointer.pointerOffset(baseAddress, loc); - - final Expression sum = mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, - pointerOffset, sizeT, fieldOffset.getAddressOffsetAsExpression(loc), sizeT); - - return mMemoryPointer.constructPointerFromBaseAndOffset(pointerBase, sum, loc); - } - @Override public Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant) { 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 19a068493b4..71fd77265d5 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 @@ -864,8 +864,11 @@ public ExpressionResult doPointerArithmeticWithConversion(final int operator, fi } public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive type) { - return mMemoryModel.constructAddressForStructField(loc, baseAddress, fieldOffset, type); + final Offset fieldOffset) { + if (fieldOffset.isBitfieldOffset()) { + throw new UnsupportedOperationException("Bitfield read"); + } + return mMemoryModel.addExpressionToPointer(loc, baseAddress, fieldOffset.getAddressOffsetAsExpression(loc)); } public void beginScope() { @@ -2037,8 +2040,7 @@ private List getWriteCallStruct(final ILocation loc, final HeapLValue throw new UnsupportedOperationException("Bitfield write"); } - final Expression newPointer = mMemoryModel.constructAddressForStructField(loc, startAddress, fieldOffset, - mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression newPointer = constructAddressForStructField(loc, startAddress, fieldOffset); final HeapLValue fieldHlv = LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, fieldType, null); final StructAccessExpression sae = ExpressionFactory.constructStructAccessExpression(loc, value, fieldId); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index f1ddba57dfb..129dfe442ec 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -39,7 +39,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.MemoryStructureBase.ReadWriteDefinition; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; 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; @@ -212,19 +211,6 @@ public BigInteger fixedAddressCounterCountingStep(final Expression size) { return mMemoryAddressing.getFixedAddressCounterCountingStep(size); } - /** - * Returns the address for struct field. - * - * @return The address. - */ - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - if (fieldOffset.isBitfieldOffset()) { - throw new UnsupportedOperationException("Bitfield read"); - } - return mMemoryAddressing.constructAddressForStructField(loc, baseAddress, fieldOffset, sizeT); - } - /** * Adds an integer to a pointer. * diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java index f360417b7e4..5aac009a694 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java @@ -130,8 +130,7 @@ public Result handleFieldReference(final IDispatcher main, final ExpressionResul // TODO: different calculations for unions final Expression startAddress = fieldOwnerHlv.getAddress(); - final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, startAddress, fieldOffset, - mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, startAddress, fieldOffset); final BitfieldInformation bi = constructBitfieldInformation(bitfieldWidth); newValue = LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, cFieldType, bi); @@ -197,8 +196,8 @@ private List computeNeighbourFieldsOfUnionField(final ILocatio final Offset fieldOffset = mTypeSizeAndOffsetComputer.constructOffsetForField(loc, foType, neighbourField); - final Expression neighbourFieldAddress = mMemoryHandler.constructAddressForStructField(loc, - unionAddress, fieldOffset, mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression neighbourFieldAddress = + mMemoryHandler.constructAddressForStructField(loc, unionAddress, fieldOffset); builder.setLrValue(LRValueFactory.constructHeapLValue(mTypeHandler, neighbourFieldAddress, foType.getFieldType(neighbourField), null)); @@ -237,8 +236,7 @@ public Expression computeStructFieldAddress(final ILocation loc, final int field } final Offset fieldOffset = mTypeSizeAndOffsetComputer.constructOffsetForField(loc, structType, fieldIndex); - return mMemoryHandler.constructAddressForStructField(loc, address, fieldOffset, - mTypeSizeAndOffsetComputer.getSizeT()); + return mMemoryHandler.constructAddressForStructField(loc, address, fieldOffset); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java index 582de331add..7bd5907c5a1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java @@ -387,8 +387,8 @@ private ExpressionResult readStructFromHeap(final ExpressionResult old, final IL throw new UnsupportedOperationException("Bitfield read struct from heap"); } - final var newAddress = mMemoryHandler.constructAddressForStructField(loc, structOnHeapAddress, - innerStructOffset, mExprTrans.getCTypeOfPointerComponents()); + final var newAddress = + mMemoryHandler.constructAddressForStructField(loc, structOnHeapAddress, innerStructOffset); final ExpressionResult fieldRead = readStructFromHeap(old, loc, newAddress, cStructOrUnion, hook, unchecked); From 6bc146ebb13d8393780effe90bd25accfe066a81 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Sat, 3 Jan 2026 12:40:18 +0100 Subject: [PATCH 18/20] allocation procedures: replace lists of tuples by meaningful record Instead of encoding the specifications of malloc, dealloc and allocInit as lists of tuples containing expressions (which are used in "ensures" resp. "free ensures" clauses) and sets of variables (which are used in the "modifies" clause), they are now encoded using a specialized record. --- .../base/chandler/IMemoryAdressing.java | 34 ++++---- .../chandler/IMemoryManagementStrategy.java | 77 +++++++++++++++---- .../base/chandler/MemoryAdressingBase.java | 35 ++++----- .../base/chandler/MemoryHandler.java | 45 +++-------- .../base/chandler/MemoryModel.java | 50 ++++++------ .../base/chandler/NonDetStrategy2D.java | 46 +++++------ .../base/chandler/ProcedureManager.java | 6 +- .../chandler/SimpleIncreasingStrategy.java | 39 +++++----- 8 files changed, 173 insertions(+), 159 deletions(-) diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index 2c835cae6ab..420458775b8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -29,7 +29,6 @@ import java.math.BigInteger; import java.util.Collection; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; @@ -38,14 +37,13 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * The interface defining the functions for the different memory addressing schemes. @@ -70,40 +68,40 @@ public interface IMemoryAdressing { List getMetaDataDeclarations(); /** - * Constructs a list of expressions that are used in the specifications of malloc. + * Constructs the specification of malloc. * - * @return The expressions. + * @return a record representing the specification */ - List>> constructMallocSpecificationExpressions(ILocation tuLoc, - MemoryArea memoryArea, RequiredMemoryModelFeatures requiredMemoryModelFeatures, + AllocationProcedureSpec constructMallocSpecification(ILocation tuLoc, MemoryArea memoryArea, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs a list of expressions that are used in the specifications of dealloc. + * Constructs the specification of dealloc. * - * @return The expressions. + * @return a record representing the specification */ - List, Boolean>> constructDeallocSpecificationExpressions(ILocation tuLoc, + AllocationProcedureSpec constructDeallocSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Returns a list of statements that are part of Ultimate.Init. + * Constructs the specification of allocInit. * - * @return The statements. + * @return a record representing the specification */ - List constructUltimateInitStatements(ILocation loc, + AllocationProcedureSpec constructAllocInitSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs the expressions used in the specifications for allocInit. + * Returns a list of statements that are part of Ultimate.Init. * - * @return The expressions. + * @return The statements. */ - List>> constructAllocInitSpecificationExpressions(ILocation tuLoc, + List constructUltimateInitStatements(ILocation loc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); /** * Add or subtracts a pointer and an integer. diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java index cb22499ef54..df7310cc82a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java @@ -27,15 +27,17 @@ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Collections; import java.util.List; +import java.util.Objects; import java.util.Set; +import de.uni_freiburg.informatik.ultimate.boogie.ast.EnsuresSpecification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This interface defines the functions for different memory management strategies. E.g. counting up, counting down, or @@ -45,20 +47,29 @@ */ public interface IMemoryManagementStrategy { /** - * Constructs a list of expressions that are used in the specifications of malloc. + * Constructs the specification of malloc. * - * @return The expressions. + * @return a record representing the specification */ - List>> constructMallocSpecificationExpressions(ILocation tuLoc, - MemoryArea memoryArea, RequiredMemoryModelFeatures requiredMemoryModelFeatures, + AllocationProcedureSpec constructMallocSpecification(ILocation tuLoc, MemoryArea memoryArea, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + + /** + * Constructs the specification of dealloc. + * + * @return a record representing the specification + */ + AllocationProcedureSpec constructDeallocSpecification(ILocation tuLoc, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs a list of expressions that are used in the specifications of dealloc. + * Constructs the specification for allocInit. * - * @return The expressions. + * @return a record representing the specification */ - List, Boolean>> constructDeallocSpecificationExpressions(ILocation tuLoc, + AllocationProcedureSpec constructAllocInitSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); @@ -72,11 +83,49 @@ List constructUltimateInitStatements(ILocation loc, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); /** - * Constructs the expressions used in the specifications for allocInit. + * Encapsulates the specification for an allocation procedure. + * + * Currently, we do not allow allocation procedures to have "requires" clauses. * - * @return The expressions. + * @param ensures + * the "ensures" clauses for the procedure + * @param freeEnsures + * the "free ensures" clauses for the procedure + * @param modifies + * the set of modified global variables of the procedure */ - List>> constructAllocInitSpecificationExpressions(ILocation tuLoc, - RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + record AllocationProcedureSpec(List ensures, List freeEnsures, Set modifies) { + /** + * Convenience constructor for specs that do not have "free ensures" clauses. + */ + AllocationProcedureSpec(final List ensures, final Set modifies) { + this(ensures, Collections.emptyList(), modifies); + } + + public AllocationProcedureSpec { + Objects.requireNonNull(ensures); + Objects.requireNonNull(freeEnsures); + Objects.requireNonNull(modifies); + } + + /** + * Constructs "requires" resp. "free requires" clauses from the expressions stored in this specification. + * + * Note: Do not forget to handle the "modifies" clauses separately! + * + * @param loc + * the location for the specification clauses + * @return the list of clauses + */ + List constructSpecificationClauses(final ILocation loc) { + final var result = new ArrayList(); + for (final Expression ens : ensures) { + result.add(new EnsuresSpecification(loc, false, ens)); + } + for (final Expression freeEns : freeEnsures) { + result.add(new EnsuresSpecification(loc, true, freeEns)); + } + return result; + } + } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index ec935e58a82..d7062b2fa98 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -28,7 +28,6 @@ import java.math.BigInteger; import java.util.List; -import java.util.Set; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; @@ -36,9 +35,9 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IPointerIntegerConversion; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.NonBijectiveMapping1D; @@ -53,8 +52,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.PointerIntegerConversion; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * Abstract base class for implementing specific memory addressing schemes based on a memory pointer representation. @@ -135,35 +132,35 @@ private Expression calculateSizeOf(final ILocation loc, final ICType cType) { } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructMallocSpecificationExpressions(tuLoc, memoryArea, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryManagementStrategy.constructMallocSpecification(tuLoc, memoryArea, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructDeallocSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, + return mMemoryManagementStrategy.constructDeallocSpecification(tuLoc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } @Override - public List constructUltimateInitStatements(final ILocation loc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { - return mMemoryManagementStrategy.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler, fixedAddressCounter); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + return mMemoryManagementStrategy.constructAllocInitSpecification(tuLoc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public List constructUltimateInitStatements(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructAllocInitSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { + return mMemoryManagementStrategy.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler, fixedAddressCounter); } @Override 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 71fd77265d5..cccc0847c5a 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 @@ -95,6 +95,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.DataRaceChecker; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.TranslationSettings; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.MemoryStructureBase.ReadWriteDefinition; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.memoryhandler.ConstructMemcpyOrMemmove; @@ -130,7 +131,6 @@ import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.MemoryStructure; import de.uni_freiburg.informatik.ultimate.util.datastructures.LinkedScopedHashMap; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * @author Markus Lindenmann @@ -1884,18 +1884,11 @@ private List declareDeallocation(final CHandler main, final ILocati mProcedureManager.beginCustomProcedure(main, tuLoc, MemoryModelDeclarations.ULTIMATE_DEALLOC.getName(), deallocDeclaration); - final List, Boolean>> deallocSpecificationExpressions = - mMemoryModel.constructDeallocSpecificationExpressions(tuLoc, mRequiredMemoryModelFeatures, - mMemoryModelDeclarationsHandler); - - final List deallocSpecifications = new ArrayList<>(); - - for (final Triple, Boolean> triple : deallocSpecificationExpressions) { - deallocSpecifications.add(mProcedureManager.constructEnsuresSpecification(tuLoc, triple.getThird(), - triple.getFirst(), triple.getSecond())); - } + final AllocationProcedureSpec specification = mMemoryModel.constructDeallocSpecification(tuLoc, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - mProcedureManager.addSpecificationsToCurrentProcedure(deallocSpecifications); mProcedureManager.endCustomProcedure(main, MemoryModelDeclarations.ULTIMATE_DEALLOC.getName()); return Collections.emptyList(); } @@ -1921,18 +1914,10 @@ private ArrayList declareMalloc(final CHandler main, final ITypeHan mProcedureManager.beginCustomProcedure(main, tuLoc, alloc.getName(), allocDeclaration); - final List>> mallocSpecificationExpressions = - mMemoryModel.constructMallocSpecificationExpressions(tuLoc, memArea, mRequiredMemoryModelFeatures, - mMemoryModelDeclarationsHandler); - - final List mallocSpecifications = new ArrayList<>(); - - for (final Pair> pair : mallocSpecificationExpressions) { - mallocSpecifications.add( - mProcedureManager.constructEnsuresSpecification(tuLoc, false, pair.getFirst(), pair.getSecond())); - } - - mProcedureManager.addSpecificationsToCurrentProcedure(mallocSpecifications); + final AllocationProcedureSpec specification = mMemoryModel.constructMallocSpecification(tuLoc, memArea, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); final ArrayList result = new ArrayList<>(); mProcedureManager.endCustomProcedure(main, alloc.getName()); @@ -1955,17 +1940,11 @@ private void declareAllocInit(final CHandler main, final ITypeHandler typeHandle mProcedureManager.beginCustomProcedure(main, tuLoc, procedureIdentifier, allocDeclaration); - final var allocInitSpecificationExpressions = mMemoryModel.constructAllocInitSpecificationExpressions(tuLoc, + final AllocationProcedureSpec specification = mMemoryModel.constructAllocInitSpecification(tuLoc, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - final List allocInitSpecifications = new ArrayList<>(); - - for (final Pair> pair : allocInitSpecificationExpressions) { - allocInitSpecifications.add( - mProcedureManager.constructEnsuresSpecification(tuLoc, false, pair.getFirst(), pair.getSecond())); - } - - mProcedureManager.addSpecificationsToCurrentProcedure(allocInitSpecifications); mProcedureManager.endCustomProcedure(main, procedureIdentifier); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 129dfe442ec..fcd23ed7c9d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -29,7 +29,6 @@ import java.math.BigInteger; import java.util.Collection; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; @@ -38,6 +37,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.MemoryStructureBase.ReadWriteDefinition; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; @@ -46,8 +46,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * The memory model consisting of a MemoryAdressing and a MemoryStructure. @@ -142,53 +140,51 @@ public List metaDataDeclarations() { } /** - * Constructs the expressions used in the specifications for malloc. + * Constructs the specification of malloc. * - * @return A list of a pair consisting of an expression and a set of the global variables that must be added to the - * modifies clause. + * @return a record representing the specification */ - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructMallocSpecificationExpressions(tuLoc, memoryArea, requiredMemoryModelFeatures, + return mMemoryAddressing.constructMallocSpecification(tuLoc, memoryArea, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** - * Constructs the expressions used in the specifications for dealloc. + * Constructs the specification of dealloc. * - * @return A list of a pair consisting of an expression and a set of the global variables that must be added to the - * modifies clause. + * @return a record representing the specification */ - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructDeallocSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, + return mMemoryAddressing.constructDeallocSpecification(tuLoc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** - * Constructs the statements used in Ultimate.Init. + * Constructs the specification of allocInit. * - * @return The statements. + * @return a record representing the specification */ - List constructUltimateInitStatements(final ILocation loc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { - return mMemoryAddressing.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler, fixedAddressCounter); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + return mMemoryAddressing.constructAllocInitSpecification(tuLoc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } /** - * Constructs the expressions used in the specifications for allocInit. + * Constructs the statements used in Ultimate.Init. * - * @return The expressions. + * @return The statements. */ - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + List constructUltimateInitStatements(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructAllocInitSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { + return mMemoryAddressing.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler, fixedAddressCounter); } /** diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java index 86ee52a8ab2..a1e55cb84b4 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java @@ -53,12 +53,10 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This strategy is the default strategy for the 2D-memory addressing scheme. The generic parameter is used to ensure - * that this strategy is only instanciated within the 2D addressing class because it is not compatible with other modes. + * that this strategy is only instantiated within the 2D addressing class because it is not compatible with other modes. * Memory addresses get a non-deterministic value, which is not used yet. * * @author Jan Körner @@ -77,8 +75,8 @@ public NonDetStrategy2D(final TypeSizes typeSizes, final ExpressionTranslation e } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var memoryAreaName = memoryArea.getMemoryStructureDeclaration().getName(); @@ -104,7 +102,7 @@ public List>> constructMallocSpecificationExpr final var resBaseExpr = ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE); - final ArrayList>> expressions = new ArrayList<>(); + final ArrayList expressions = new ArrayList<>(); // old(#valid)[#res!base] == false final var freshLocationCurrentlyNotValidExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, @@ -112,32 +110,30 @@ public List>> constructMallocSpecificationExpr ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, validArrayExpr), new Expression[] { resBaseExpr }), falseExpr); - - expressions.add(new Pair<>(freshLocationCurrentlyNotValidExpr, Collections.emptySet())); + expressions.add(freshLocationCurrentlyNotValidExpr); // #valid == old(#valid)[#res!base := true] final var validUpdateExpr = MemoryModelExpressionHelper.ensuresArrayUpdate(tuLoc, trueExpr, resBaseExpr, validArrayExpr); - expressions.add(new Pair<>(validUpdateExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr)))); + expressions.add(validUpdateExpr); // #res!offset == 0 final var offsetEqualZeroExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, mMemoryAddressing.mMemoryPointer.pointerOffset(resultExpr, tuLoc), zeroNumericValueExpr); - expressions.add(new Pair<>(offsetEqualZeroExpr, Collections.emptySet())); + expressions.add(offsetEqualZeroExpr); // #res!base != 0 final var baseNotEqualZeroExpr = baseNotEqualZeroExpr(tuLoc, resultExpr, zeroNumericValueExpr); - expressions.add(new Pair<>(baseNotEqualZeroExpr, Collections.emptySet())); + expressions.add(baseNotEqualZeroExpr); if (memoryArea == MemoryArea.STACK) { // #StackHeapBarrier < res!base final var baseGreaterThanBarrierExpr = baseGreaterThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseGreaterThanBarrierExpr, Collections.emptySet())); + expressions.add(baseGreaterThanBarrierExpr); } else if (memoryArea == MemoryArea.HEAP) { // res!base < #StackHeapBarrier final var baseSmallerThanBarrierExpr = baseSmallerThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseSmallerThanBarrierExpr, Collections.emptySet())); + expressions.add(baseSmallerThanBarrierExpr); } // #length == old(#length)[#res!base := ~size] @@ -148,15 +144,16 @@ public List>> constructMallocSpecificationExpr tuLoc, ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, lengthArrayExpr), new Expression[] { resBaseExpr }, sizeExpr)); - expressions.add(new Pair<>(lengthUpdateExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(lengthArrayExpr)))); + expressions.add(lengthUpdateExpr); - return expressions; + final var validArrayLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr); + final var lengthArrayLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(lengthArrayExpr); + return new AllocationProcedureSpec(expressions, Set.of(validArrayLHS, lengthArrayLHS)); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var falseExpr = mBooleanArrayHelper.constructFalse(); @@ -178,8 +175,8 @@ public List, Boolean>> constructDeallocSpeci final Expression updateValidArrayExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, validArrayExpr, arrayStoreExpr); - return Collections.singletonList(new Triple<>(updateValidArrayExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr)), true)); + return new AllocationProcedureSpec(Collections.emptyList(), List.of(updateValidArrayExpr), + Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr))); } @Override @@ -236,7 +233,7 @@ public List constructUltimateInitStatements(final ILocation loc, } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var pointerBaseIdentifier = "ptrBase"; @@ -254,18 +251,15 @@ public List>> constructAllocInitSpecificationE mTypeHandler.getBoogieTypeForPointerComponents(), pointerBaseIdentifier, new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureIdentifier)); - final ArrayList>> expressions = new ArrayList<>(); // ensures #valid[ptrBase] == true; final var validPtrBaseExpr = MemoryModelExpressionHelper.ensuresArrayHasValue(tuLoc, trueExpr, ptrBase, validArrayExpr); - expressions.add(new Pair<>(validPtrBaseExpr, Collections.emptySet())); // ensures #length[ptrBase] == size; final var lengthPtrBaseSize = MemoryModelExpressionHelper.ensuresArrayHasValue(tuLoc, size, ptrBase, lengthArrayExpr); - expressions.add(new Pair<>(lengthPtrBaseSize, Collections.emptySet())); - return expressions; + return new AllocationProcedureSpec(List.of(validPtrBaseExpr, lengthPtrBaseSize), Collections.emptySet()); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java index 613a3d4b716..64a68a9fbbf 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java @@ -453,7 +453,11 @@ public EnsuresSpecification constructEnsuresSpecification(final ILocation loc, f return new EnsuresSpecification(loc, isFree, formula); } - public void addSpecificationsToCurrentProcedure(final List specs) { + public void addModifiedGlobalsToCurrentProcedure(final Set modifiedGlobals) { + mCurrentProcedureInfo.addModifiedGlobals(modifiedGlobals); + } + + public void addSpecificationsToCurrentProcedure(final List specs) { assert !isGlobalScope(); final BoogieProcedureInfo procInfo = mCurrentProcedureInfo; final Procedure oldDecl = procInfo.getDeclaration(); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java index 2c729184ad5..268da36d803 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java @@ -48,8 +48,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This strategy is the default strategy for the 1D-memory addressing scheme. The generic parameter is used to ensure @@ -69,12 +67,12 @@ public SimpleIncreasingStrategy(final TypeSizes typeSizes, final ExpressionTrans } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); - final ArrayList>> expressions = new ArrayList<>(); + final ArrayList expressions = new ArrayList<>(); final var memoryAreaName = memoryArea.getMemoryStructureDeclaration().getName(); final var zeroNumericValueExpr = @@ -104,7 +102,7 @@ public List>> constructMallocSpecificationExpr // #res!base == old(counterExpression); final var baseEqualCounterExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, resBaseExpr, ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, counterExpression)); - expressions.add(new Pair<>(baseEqualCounterExpr, Collections.emptySet())); + expressions.add(baseEqualCounterExpr); // #res!base > 0; final var baseGreaterZeroExpr = mExpressionTranslation.constructBinaryComparisonIntegerExpression(tuLoc, @@ -112,18 +110,18 @@ public List>> constructMallocSpecificationExpr ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE), cTypeOfPointerComponent, zeroNumericValueExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(baseGreaterZeroExpr, Collections.emptySet())); + expressions.add(baseGreaterZeroExpr); if (memoryArea == MemoryArea.STACK) { // res!base > #StackHeapBarrier final var baseGreaterThanBarrierExpr = baseGreaterThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseGreaterThanBarrierExpr, Collections.emptySet())); + expressions.add(baseGreaterThanBarrierExpr); // #StackAllocations > #StackHeapBarrier; final var stackAllocationsGreaterThanBarrier = mExpressionTranslation .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_greaterThan, counterExpression, cTypeOfPointerComponent, stackHeapBarrierExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsGreaterThanBarrier, Collections.emptySet())); + expressions.add(stackAllocationsGreaterThanBarrier); // #StackAllocations < #32-bit max / 64-bit max if (mIsBitVectorTranslation) { @@ -139,19 +137,19 @@ public List>> constructMallocSpecificationExpr .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_lessThan, counterExpression, cTypeOfPointerComponent, maxExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsSmallerThanMax, Collections.emptySet())); + expressions.add(stackAllocationsSmallerThanMax); } } else if (memoryArea == MemoryArea.HEAP) { // res!base < #StackHeapBarrier final var baseSmallerThanBarrierExpr = baseSmallerThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseSmallerThanBarrierExpr, Collections.emptySet())); + expressions.add(baseSmallerThanBarrierExpr); // #HeapAllocations < #StackHeapBarrier; final var stackAllocationsGreaterThanBarrier = mExpressionTranslation .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_lessThan, counterExpression, cTypeOfPointerComponent, stackHeapBarrierExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsGreaterThanBarrier, Collections.emptySet())); + expressions.add(stackAllocationsGreaterThanBarrier); } // res!base > #InitialAllocation @@ -159,7 +157,7 @@ public List>> constructMallocSpecificationExpr tuLoc, IASTBinaryExpression.op_greaterThan, ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE), cTypeOfPointerComponent, initialAllocCounterExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(baseGreaterThanInitialAllocsExpr, Collections.emptySet())); + expressions.add(baseGreaterThanInitialAllocsExpr); // StackAllocations == old(StackAllocations) + ~size // HeapAllocations == old(HeapAllocations) + ~size @@ -169,18 +167,17 @@ public List>> constructMallocSpecificationExpr oldExpr, cTypeOfPointerComponent, sizeExpr, mTypeSizeAndOffsetComputer.getSizeT()); final var counterUpdateValueExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, counterExpression, sumExpr); + expressions.add(counterUpdateValueExpr); - expressions.add(new Pair<>(counterUpdateValueExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(counterExpression)))); - - return expressions; + final var counterLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(counterExpression); + return new AllocationProcedureSpec(expressions, Set.of(counterLHS)); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return Collections.emptyList(); + return new AllocationProcedureSpec(Collections.emptyList(), Collections.emptySet()); } @Override @@ -218,10 +215,10 @@ public List constructUltimateInitStatements(final ILocation loc, } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return Collections.emptyList(); + return new AllocationProcedureSpec(Collections.emptyList(), Collections.emptySet()); } } From 15a9ef8be1b5ce864209a5f863fb31c4c8a0ed40 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Sat, 3 Jan 2026 12:53:07 +0100 Subject: [PATCH 19/20] move "ptrBase" string constant to SFO --- .../implementation/base/chandler/MemoryHandler.java | 3 +-- .../implementation/base/chandler/NonDetStrategy2D.java | 3 +-- .../ultimate/cdt/translation/implementation/util/SFO.java | 2 ++ 3 files changed, 4 insertions(+), 4 deletions(-) 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 cccc0847c5a..748c475d21b 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 @@ -1931,11 +1931,10 @@ private ArrayList declareMalloc(final CHandler main, final ITypeHan */ private void declareAllocInit(final CHandler main, final ITypeHandler typeHandler, final ILocation tuLoc) { final String procedureIdentifier = MemoryModelDeclarations.ULTIMATE_ALLOC_INIT.getName(); - final String pointerBaseIdentifier = "ptrBase"; final ASTType intType = typeHandler.cType2AstType(tuLoc, mExpressionTranslation.getCTypeOfPointerComponents()); final Procedure allocDeclaration = new Procedure(tuLoc, new Attribute[0], procedureIdentifier, new String[0], - new VarList[] { new VarList(tuLoc, new String[] { SFO.SIZE, pointerBaseIdentifier }, intType) }, + new VarList[] { new VarList(tuLoc, new String[] { SFO.SIZE, SFO.ALLOCINIT_PTRBASE }, intType) }, new VarList[0], new Specification[0], null); mProcedureManager.beginCustomProcedure(main, tuLoc, procedureIdentifier, allocDeclaration); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java index a1e55cb84b4..c1786b016fa 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java @@ -236,7 +236,6 @@ public List constructUltimateInitStatements(final ILocation loc, public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - final var pointerBaseIdentifier = "ptrBase"; final var procedureIdentifier = MemoryModelDeclarations.ULTIMATE_ALLOC_INIT.getName(); final var trueExpr = mBooleanArrayHelper.constructTrue(); @@ -248,7 +247,7 @@ public AllocationProcedureSpec constructAllocInitSpecification(final ILocation t SFO.SIZE, new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureIdentifier)); final var ptrBase = ExpressionFactory.constructIdentifierExpression(tuLoc, - mTypeHandler.getBoogieTypeForPointerComponents(), pointerBaseIdentifier, + mTypeHandler.getBoogieTypeForPointerComponents(), SFO.ALLOCINIT_PTRBASE, new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureIdentifier)); // ensures #valid[ptrBase] == true; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java index 26cab160172..8a3d00ce566 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java @@ -183,6 +183,8 @@ public final class SFO { public static final String STRCPY_DEST = "dest"; public static final String STRCPY_SRC = "src"; + public static final String ALLOCINIT_PTRBASE = "ptrBase"; + public static final String TO_INT = "#to_int"; /** From 7f5e455baa6dd87862ea3ed5389f22f4c5147569 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Sat, 3 Jan 2026 12:53:58 +0100 Subject: [PATCH 20/20] MemoryHandler: minor internal refactoring, removing some unused code --- .../base/chandler/MemoryHandler.java | 57 +++++-------------- 1 file changed, 15 insertions(+), 42 deletions(-) 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 748c475d21b..5cee2d393f3 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 @@ -302,8 +302,8 @@ public List declareMemoryStructureInfrastructure(final CHandler mai declarations .add(constructMemoryArrayDeclaration(tuLoc, heapDataArray.getName(), heapDataArray.getASTType())); // create and add read and write procedure - declarations.addAll(constructWriteProcedures(main, tuLoc, heapDataArrays, heapDataArray)); - declarations.addAll(constructReadProcedures(main, tuLoc, heapDataArray)); + constructWriteProcedures(main, tuLoc, heapDataArrays, heapDataArray); + constructReadProcedures(main, tuLoc, heapDataArray); } // add store function (to be able to assign subarrays at pointer base addresses) @@ -328,11 +328,11 @@ public List declareMemoryStructureInfrastructure(final CHandler mai declareDataOnHeapInitFunction(mMemoryModel.getPointerHeapArray()); } - declarations.addAll(declareDeallocation(main, tuLoc)); + declareDeallocation(main, tuLoc); if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() .contains(MemoryModelDeclarations.ULTIMATE_ALLOC_STACK)) { - declarations.addAll(declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.STACK)); + declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.STACK); } if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() @@ -342,7 +342,7 @@ public List declareMemoryStructureInfrastructure(final CHandler mai if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() .contains(MemoryModelDeclarations.ULTIMATE_ALLOC_HEAP)) { - declarations.addAll(declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.HEAP)); + declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.HEAP); } if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() @@ -1445,26 +1445,19 @@ private VariableDeclaration constructDeclOfPointerIndexedArray(final ILocation l return new VariableDeclaration(loc, new Attribute[0], new VarList[] { varList }); } - private List constructWriteProcedures(final CHandler main, final ILocation loc, + private void constructWriteProcedures(final CHandler main, final ILocation loc, final Collection heapDataArrays, final HeapDataArray heapDataArray) { - final List result = new ArrayList<>(); for (final ReadWriteDefinition rda : mMemoryModel.getReadWriteDefinitionForHeapDataArray(heapDataArray, mRequiredMemoryModelFeatures)) { - final Collection writeDeclaration = - constructWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda); - result.addAll(writeDeclaration); + constructWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda); } - return result; } - private List constructReadProcedures(final CHandler main, final ILocation loc, - final HeapDataArray heapDataArray) { - final List result = new ArrayList<>(); + private void constructReadProcedures(final CHandler main, final ILocation loc, final HeapDataArray heapDataArray) { for (final ReadWriteDefinition rda : mMemoryModel.getReadWriteDefinitionForHeapDataArray(heapDataArray, mRequiredMemoryModelFeatures)) { - result.addAll(constructSingleReadProcedure(main, loc, heapDataArray, rda)); + constructSingleReadProcedure(main, loc, heapDataArray, rda); } - return result; } private VariableDeclaration declarePthreadsForkCount(final ILocation loc) { @@ -1499,7 +1492,7 @@ private VariableDeclaration declarePthreadRwLock(final ILocation loc) { * @param rda * @return */ - private Collection constructWriteProcedure(final CHandler main, final ILocation loc, + private void constructWriteProcedure(final CHandler main, final ILocation loc, final Collection heapDataArrays, final HeapDataArray heapDataArray, final ReadWriteDefinition rda) { if (rda.alsoUncheckedWrite()) { @@ -1509,7 +1502,6 @@ private Collection constructWriteProcedure(final CHandler main, final constructSingleWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda, HeapWriteMode.SELECT); } constructSingleWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda, HeapWriteMode.STORE_CHECKED); - return Collections.emptySet(); } private void constructSingleWriteProcedure(final CHandler main, final ILocation loc, @@ -1671,8 +1663,8 @@ private static List constructConjunctsForWriteEnsuresSpecification(f * whether we should construct an unchecked read procedure (i.e. one that omits validity checks) * @return */ - private List constructSingleReadProcedure(final CHandler main, final ILocation loc, - final HeapDataArray hda, final ReadWriteDefinition rda) { + private void constructSingleReadProcedure(final CHandler main, final ILocation loc, final HeapDataArray hda, + final ReadWriteDefinition rda) { // specification for memory reads final String returnValue = "#value"; final ASTType valueAstType = rda.getASTType(); @@ -1718,8 +1710,6 @@ private List constructSingleReadProcedure(final CHandler main, final mProcedureManager.addSpecificationsToCurrentProcedure(sread); mProcedureManager.endCustomProcedure(main, readProcedureName); - - return Collections.emptyList(); } private Expression readFromHeap(final ILocation loc, final HeapDataArray hda, final Expression address, @@ -1851,19 +1841,6 @@ public List constructPointerBaseValidityCheck(final ILocation loc return Collections.singletonList(spec); } - /** - * Compare a pointer component (base or offset) to another expression. - * - * @param op - * One of the comparison operators defined in {@link IASTBinaryExpression}. - */ - private Expression constructPointerBinaryComparisonExpression(final ILocation loc, final int op, - final Expression left, final Expression right) { - return mExpressionTranslation.constructBinaryComparisonExpression(loc, op, left, - mExpressionTranslation.getCTypeOfPointerComponents(), right, - mExpressionTranslation.getCTypeOfPointerComponents()); - } - /** * Generate procedure ULTIMATE.dealloc(~addr:$Pointer$) returns()'s declaration and implementation. * This procedure should be used for deallocations where do not want to check if given memory area is valid (because @@ -1874,8 +1851,7 @@ private Expression constructPointerBinaryComparisonExpression(final ILocation lo * * @return declaration and implementation of procedure Ultimate_dealloc */ - private List declareDeallocation(final CHandler main, final ILocation tuLoc) { - + private void declareDeallocation(final CHandler main, final ILocation tuLoc) { final Procedure deallocDeclaration = new Procedure(tuLoc, new Attribute[0], MemoryModelDeclarations.ULTIMATE_DEALLOC.getName(), new String[0], new VarList[] { @@ -1890,7 +1866,6 @@ private List declareDeallocation(final CHandler main, final ILocati mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); mProcedureManager.endCustomProcedure(main, MemoryModelDeclarations.ULTIMATE_DEALLOC.getName()); - return Collections.emptyList(); } /** @@ -1903,8 +1878,8 @@ private List declareDeallocation(final CHandler main, final ILocati * * @return declaration and implementation of procedure ~malloc */ - private ArrayList declareMalloc(final CHandler main, final ITypeHandler typeHandler, - final ILocation tuLoc, final MemoryArea memArea) { + private void declareMalloc(final CHandler main, final ITypeHandler typeHandler, final ILocation tuLoc, + final MemoryArea memArea) { final MemoryModelDeclarations alloc = memArea.getMemoryStructureDeclaration(); final ASTType intType = typeHandler.cType2AstType(tuLoc, mExpressionTranslation.getCTypeOfPointerComponents()); final Procedure allocDeclaration = new Procedure(tuLoc, new Attribute[0], alloc.getName(), new String[0], @@ -1919,9 +1894,7 @@ private ArrayList declareMalloc(final CHandler main, final ITypeHan mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - final ArrayList result = new ArrayList<>(); mProcedureManager.endCustomProcedure(main, alloc.getName()); - return result; } /**