Skip to content

Use call as location for error node corresponding to requires #730

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
schuessf wants to merge 3 commits into
base: dev
Choose a base branch
from
Draft

Use call as location for error node corresponding to requires #730

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
25300ad
Use call as location for error node corresponding to requires
schuessf Jun 17, 2025
2573353
Bugfix: Pass Check separately, use Check from requires
schuessf Jun 18, 2025
488e30f
Minor
schuessf Jun 18, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 13 additions & 13 deletions ...src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -438,8 +437,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<DebugIdentifier, BoogieIcfgLocation> procLocNodes) {
if (check == null) {
throw new IllegalArgumentException(
"Constructing error location without specification for the following AST node: " + boogieASTNode);
}
Set<BoogieIcfgLocation> errorNodes = mIcfg.getProcedureErrorNodes().get(procName);
final int locNodeNumber;
if (errorNodes == null) {
Expand All @@ -455,7 +458,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;
Expand All @@ -465,13 +468,7 @@ 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 var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode);
check.annotate(errorLocNode);
procLocNodes.put(errorLocLabel, errorLocNode);
Expand Down Expand Up @@ -1008,7 +1005,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) {
Expand Down Expand Up @@ -1265,7 +1263,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, spec, mProcLocNodes);
final BoogieIcfgLocation errorLocNode =
addErrorNode(mCurrentProcedureName, st, Check.getAnnotation(spec), mProcLocNodes);
final StatementSequence errorCB =
mCbf.constructStatementSequence(newLocation, errorLocNode, assumeSt);
ModelUtils.copyAnnotations(spec, errorCB);
Expand Down Expand Up @@ -1532,7 +1531,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);
Expand Down
26 changes: 13 additions & 13 deletions ...src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -413,8 +412,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<DebugIdentifier, BoogieIcfgLocation> procLocNodes) {
if (check == null) {
throw new IllegalArgumentException(
"Constructing error location without specification for the following AST node: " + boogieASTNode);
}
Set<BoogieIcfgLocation> errorNodes = mIcfg.getProcedureErrorNodes().get(procName);
final int locNodeNumber;
if (errorNodes == null) {
Expand All @@ -430,21 +433,15 @@ 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;
} else {
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 var errorLocLabel = new ProcedureErrorWithCheckDebugIdentifier(procName, locNodeNumber, type, check);
final BoogieIcfgLocation errorLocNode = new BoogieIcfgLocation(errorLocLabel, procName, true, boogieASTNode);
check.annotate(errorLocNode);
procLocNodes.put(errorLocLabel, errorLocNode);
Expand Down Expand Up @@ -1021,7 +1018,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);
Expand Down Expand Up @@ -1248,7 +1246,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);
Expand Down Expand Up @@ -1394,7 +1393,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, spec, 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);
Expand Down