Skip to content

Commit

Permalink
Inline method
Browse files Browse the repository at this point in the history
  • Loading branch information
Heizmann committed Aug 29, 2024
1 parent ba104cf commit f13a388
Showing 1 changed file with 4 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1120,11 +1120,6 @@ private BoogieIcfgLocation buildJoin(final BoogieIcfgLocation currentLocation, f
return newLocation;
}

private IIcfgElement beginAtomicBlockFromBottom(final BoogieIcfgLocation currentLocation) {
AtomicBlockInfo.addEndAnnotation(currentLocation);
return currentLocation;
}

private BoogieIcfgLocation endAtomicBlockAtTop(IIcfgElement curElement, final Statement st) {
if (!(curElement instanceof StatementSequence)) {
curElement = startNewStatementSequence((BoogieIcfgLocation) curElement, Origin.IMPLEMENTATION);
Expand All @@ -1142,8 +1137,8 @@ private BoogieIcfgLocation endAtomicBlockAtTop(IIcfgElement curElement, final St
}

private BoogieIcfgLocation buildAtomic(final BoogieIcfgLocation currentLocation, final AtomicStatement st) {
IIcfgElement curElement = beginAtomicBlockFromBottom(currentLocation);
curElement = buildCodeBlock(st.getBody(), curElement, false);
AtomicBlockInfo.addEndAnnotation(currentLocation);
final IIcfgElement curElement = buildCodeBlock(st.getBody(), currentLocation, false);
return endAtomicBlockAtTop(curElement, st);
}

Expand All @@ -1161,7 +1156,8 @@ private IIcfgElement buildCall(final IIcfgElement currentLocation, final CallSta
} else {
throw new AssertionError("Expected StatementSequence or BoogieIcfgLocation");
}
return beginAtomicBlockFromBottom(locAfterAtomicBlock);
AtomicBlockInfo.addEndAnnotation(locAfterAtomicBlock);
return locAfterAtomicBlock;
}

final List<RequiresSpecification> requiresNonFree = mBoogieDeclarations.getRequiresNonFree().get(callee);
Expand Down

0 comments on commit f13a388

Please sign in to comment.