[PExplicit] Throw error if number of choices in choose(.) exceeds 10K

p-org · May 6, 2024 · 3069833 · 3069833
1 parent 868cbd6
commit 3069833
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java
@@ -7,6 +7,7 @@
 import pexplicit.runtime.machine.PMachine;
 import pexplicit.runtime.machine.PMonitor;
 import pexplicit.runtime.scheduler.explicit.StepState;
+import pexplicit.utils.exceptions.BugFoundException;
 import pexplicit.utils.exceptions.NotImplementedException;
 import pexplicit.utils.misc.Assert;
 import pexplicit.values.*;
@@ -146,6 +147,9 @@ public PBool getRandomBool() {
     public PInt getRandomInt(PInt bound) {
         List<PValue<?>> choices = new ArrayList<>();
         int boundInt = bound.getValue();
+        if (boundInt > 10000) {
+            throw new BugFoundException(String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", boundInt));
+        }
         if (boundInt == 0) {
             boundInt = 1;
         }