make sure nodatarace-LBE is only used for concurrent programs

The setting "Only consider context switches at boundaries of atomic blocks" (aka the nodatarace-LBE) is only meant to affect concurrent programs. It performs a kind of large-block encoding (LBE) that is usually not desirable for sequential programs.
ultimate-pa · Nov 4, 2024 · d00bf86 · d00bf86
1 parent 7d29f53
commit d00bf86
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java b/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/icfgbuilder/cfg/CfgBuilder.java
@@ -102,6 +102,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.BoogieDeclarations;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.boogie.Statements2TransFormula.TranslationResult;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.ConcurrencyInformation;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.IcfgUtils;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.ThreadInstance;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgElement;
@@ -324,7 +325,8 @@ public IIcfg<BoogieIcfgLocation> createIcfg(final Unit unit) {
 		case SequenceOfStatements: // handled in ProcedureCfgBuilder
 		case OneNontrivialStatement:
 		case SingleStatement:
-			final var internalMode = mCtxSwitchOnlyAtAtomicBoundaries ? InternalLbeMode.ALL_EXCEPT_ATOMIC_BOUNDARIES
+			final var internalMode = mCtxSwitchOnlyAtAtomicBoundaries && IcfgUtils.isConcurrent(mIcfg)
+					? InternalLbeMode.ALL_EXCEPT_ATOMIC_BOUNDARIES
 					: InternalLbeMode.ONLY_ATOMIC_BLOCK;
 			new LargeBlockEncoding(mServices, mIcfg, mCbf, internalMode);
 			break;

diff --git a/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
@@ -288,7 +288,8 @@ public IIcfg<BoogieIcfgLocation> createIcfg(final Unit unit) {
 		case SequenceOfStatements: // handled in ProcedureCfgBuilder
 		case OneNontrivialStatement:
 		case SingleStatement:
-			final var internalMode = mCtxSwitchOnlyAtAtomicBoundaries ? InternalLbeMode.ALL_EXCEPT_ATOMIC_BOUNDARIES
+			final var internalMode = mCtxSwitchOnlyAtAtomicBoundaries && IcfgUtils.isConcurrent(mIcfg)
+					? InternalLbeMode.ALL_EXCEPT_ATOMIC_BOUNDARIES
 					: InternalLbeMode.ONLY_ATOMIC_BLOCK;
 			new LargeBlockEncoding(mServices, mIcfg, mCbf, internalMode);
 			break;