From 0e78147c69464d61fbdf0d83a8d6b929462e7ae5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 17 Jun 2025 10:06:17 +0200 Subject: [PATCH 1/4] Use call as location for error node corresponding to requires This reverts commit bb54f4c for RCFGBuilder and applies the same patch for IcfgBuilder. --- .../plugins/generator/icfgbuilder/cfg/CfgBuilder.java | 4 ++-- .../plugins/generator/rcfgbuilder/cfg/CfgBuilder.java | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java index fe18431195a..d0182938dea 100644 --- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java @@ -462,7 +462,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo type = ProcedureErrorType.ASSERT_VIOLATION; } else if (boogieASTNode instanceof EnsuresSpecification) { type = ProcedureErrorType.ENSURES_VIOLATION; - } else if (boogieASTNode instanceof RequiresSpecification) { + } else if (boogieASTNode instanceof CallStatement) { type = ProcedureErrorType.REQUIRES_VIOLATION; } else if (boogieASTNode instanceof ForkStatement) { type = ProcedureErrorType.INUSE_VIOLATION; @@ -1282,7 +1282,7 @@ private IIcfgElement buildCall(final IIcfgElement currentLocation, final CallSta final Statement st1 = assumeSt; ModelUtils.copyAnnotations(st, st1); mIcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes); final StatementSequence errorCB = mCbf.constructStatementSequence(newLocation, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 3f52c0be61b..727d859d3a4 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -437,7 +437,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo type = ProcedureErrorType.ASSERT_VIOLATION; } else if (boogieASTNode instanceof EnsuresSpecification) { type = ProcedureErrorType.ENSURES_VIOLATION; - } else if (boogieASTNode instanceof RequiresSpecification) { + } else if (boogieASTNode instanceof CallStatement) { type = ProcedureErrorType.REQUIRES_VIOLATION; } else if (boogieASTNode instanceof ForkStatement) { type = ProcedureErrorType.INUSE_VIOLATION; @@ -1401,7 +1401,7 @@ private void processCallStatement(final CallStatement st) { final Statement st1 = assumeSt; ModelUtils.copyAnnotations(st, st1); mRcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes); final StatementSequence errorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); ModelUtils.copyAnnotations(spec, errorLocNode); From 65716de647db86283ae3b373dd2672776bae865f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 18 Jun 2025 11:16:46 +0200 Subject: [PATCH 2/4] Bugfix: Pass Check separately, use Check from requires --- .../generator/icfgbuilder/cfg/CfgBuilder.java | 24 ++++++++++--------- .../generator/rcfgbuilder/cfg/CfgBuilder.java | 24 ++++++++++--------- 2 files changed, 26 insertions(+), 22 deletions(-) diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java index d0182938dea..664d3e48b22 100644 --- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java @@ -445,8 +445,12 @@ private void addCallTransitionAndReturnTransition(final Summary edge, * * @return */ - private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, + private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, final Check check, final Map procLocNodes) { + if (check == null) { + throw new IllegalArgumentException( + "Constructing error location without specification for the following AST node: " + boogieASTNode); + } Set errorNodes = mIcfg.getProcedureErrorNodes().get(procName); final int locNodeNumber; if (errorNodes == null) { @@ -472,13 +476,8 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo throw new IllegalArgumentException(); } - final ProcedureErrorDebugIdentifier errorLocLabel; - final Check check = Check.getAnnotation(boogieASTNode); - if (check == null) { - throw new IllegalArgumentException( - "Constructing error location without specification for the following AST node: " + boogieASTNode); - } - errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); + final ProcedureErrorDebugIdentifier errorLocLabel = + new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode); check.annotate(errorLocNode); procLocNodes.put(errorLocLabel, errorLocNode); @@ -1025,7 +1024,8 @@ private BoogieIcfgLocation buildAssert(final IIcfgElement currentElement, final private BoogieIcfgLocation buildBranchingToNewErrorLocation(final IIcfgElement currentElement, final Expression formula, final BoogieASTNode origin) { - final BoogieIcfgLocation error = addErrorNode(mCurrentProcedureName, origin, mProcLocNodes); + final BoogieIcfgLocation error = + addErrorNode(mCurrentProcedureName, origin, Check.getAnnotation(origin), mProcLocNodes); mProcLocNodes.put(error.getDebugIdentifier(), error); final AssumeStatement condNotError; if (mAddAssumeForEachAssert) { @@ -1282,7 +1282,8 @@ private IIcfgElement buildCall(final IIcfgElement currentLocation, final CallSta final Statement st1 = assumeSt; ModelUtils.copyAnnotations(st, st1); mIcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = + addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes); final StatementSequence errorCB = mCbf.constructStatementSequence(newLocation, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); @@ -1550,7 +1551,8 @@ private void assertAndAssumeEnsures() { final Statement st = assumeSt; ModelUtils.copyAnnotations(spec, st); mIcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = + addErrorNode(mCurrentProcedureName, spec, Check.getAnnotation(spec), mProcLocNodes); final CodeBlock assumeEdge = mCbf.constructStatementSequence(finalNode, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, assumeEdge); ModelUtils.copyAnnotations(spec, errorLocNode); diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 727d859d3a4..0f649ee144e 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -420,8 +420,12 @@ private void addCallTransitionAndReturnTransition(final Summary edge, * * @return */ - private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, + private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNode boogieASTNode, final Check check, final Map procLocNodes) { + if (check == null) { + throw new IllegalArgumentException( + "Constructing error location without specification for the following AST node: " + boogieASTNode); + } Set errorNodes = mIcfg.getProcedureErrorNodes().get(procName); final int locNodeNumber; if (errorNodes == null) { @@ -445,13 +449,8 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo throw new IllegalArgumentException(); } - final ProcedureErrorDebugIdentifier errorLocLabel; - final Check check = Check.getAnnotation(boogieASTNode); - if (check == null) { - throw new IllegalArgumentException( - "Constructing error location without specification for the following AST node: " + boogieASTNode); - } - errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); + final ProcedureErrorDebugIdentifier errorLocLabel = + new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode); check.annotate(errorLocNode); procLocNodes.put(errorLocLabel, errorLocNode); @@ -1028,7 +1027,8 @@ private void assertAndAssumeEnsures() { final Statement st = assumeSt; ModelUtils.copyAnnotations(spec, st); mRcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, spec, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = + addErrorNode(mCurrentProcedureName, spec, Check.getAnnotation(spec), mProcLocNodes); final CodeBlock assumeEdge = mCbf.constructStatementSequence(finalNode, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, assumeEdge); ModelUtils.copyAnnotations(spec, errorLocNode); @@ -1255,7 +1255,8 @@ private void processAssertStatement(final AssertStatement st) { final AssumeStatement assumeError = new AssumeStatement(st.getLocation(), getNegation(assertion)); ModelUtils.copyAnnotations(st, assumeError); mRcfgBacktranslator.putAux(assumeError, new BoogieASTNode[] { st }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = + addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(st), mProcLocNodes); final StatementSequence assumeErrorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeError); ModelUtils.copyAnnotations(st, errorLocNode); ModelUtils.copyAnnotations(st, assumeErrorCB); @@ -1401,7 +1402,8 @@ private void processCallStatement(final CallStatement st) { final Statement st1 = assumeSt; ModelUtils.copyAnnotations(st, st1); mRcfgBacktranslator.putAux(assumeSt, new BoogieASTNode[] { st, spec }); - final BoogieIcfgLocation errorLocNode = addErrorNode(mCurrentProcedureName, st, mProcLocNodes); + final BoogieIcfgLocation errorLocNode = + addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes); final StatementSequence errorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); ModelUtils.copyAnnotations(spec, errorLocNode); From 3cf3fc3372bc1635d890d310236b49e25da1136e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Wed, 18 Jun 2025 12:16:40 +0200 Subject: [PATCH 3/4] Minor --- .../plugins/generator/icfgbuilder/cfg/CfgBuilder.java | 4 +--- .../plugins/generator/rcfgbuilder/cfg/CfgBuilder.java | 4 +--- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java index 664d3e48b22..39330f175ad 100644 --- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java @@ -111,7 +111,6 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.LoopEntryDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.OrdinaryDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureEntryDebugIdentifier; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier.ProcedureErrorType; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorWithCheckDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureExitDebugIdentifier; @@ -476,8 +475,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo throw new IllegalArgumentException(); } - final ProcedureErrorDebugIdentifier errorLocLabel = - new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); + final var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode); check.annotate(errorLocNode); procLocNodes.put(errorLocLabel, errorLocNode); diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 0f649ee144e..4c7ca061927 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -101,7 +101,6 @@ import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.LoopEntryDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.OrdinaryDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureEntryDebugIdentifier; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorDebugIdentifier.ProcedureErrorType; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureErrorWithCheckDebugIdentifier; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.debugidentifiers.ProcedureExitDebugIdentifier; @@ -449,8 +448,7 @@ private BoogieIcfgLocation addErrorNode(final String procName, final BoogieASTNo throw new IllegalArgumentException(); } - final ProcedureErrorDebugIdentifier errorLocLabel = - new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); + final var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check); final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode); check.annotate(errorLocNode); procLocNodes.put(errorLocLabel, errorLocNode); From b2789d03e7f2631ffbe987ba1d2be34954bb3c11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 27 Jan 2026 18:11:47 +0100 Subject: [PATCH 4/4] Avoid copying location of requires --- .../ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java | 2 +- .../ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java index 39330f175ad..4f0c99c1c14 100644 --- a/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/IcfgBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java @@ -1285,7 +1285,7 @@ private IIcfgElement buildCall(final IIcfgElement currentLocation, final CallSta final StatementSequence errorCB = mCbf.constructStatementSequence(newLocation, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); - ModelUtils.copyAnnotations(spec, errorLocNode); + ModelUtils.copyAnnotationsExcept(spec, errorLocNode, ILocation.class); mEdges.add(errorCB); } } diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 4c7ca061927..015e15a5799 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -1404,7 +1404,7 @@ private void processCallStatement(final CallStatement st) { addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes); final StatementSequence errorCB = mCbf.constructStatementSequence(locNode, errorLocNode, assumeSt); ModelUtils.copyAnnotations(spec, errorCB); - ModelUtils.copyAnnotations(spec, errorLocNode); + ModelUtils.copyAnnotationsExcept(spec, errorLocNode, ILocation.class); mEdges.add(errorCB); } }