Add debug assertion to prevent blocking a thread on the GenMC side twice

Patrick-6 · Patrick-6 · commit 2d73543ebf10 · 2025-10-06T17:15:27.000+02:00
diff --git a/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
@@ -33,6 +33,7 @@
 /**** Blocking instructions ****/
 
 void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
+    BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
     GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::User);
 }
 

Original file line number	Diff line number	Diff line change
`@@ -33,6 +33,7 @@`
`33`	`33`	`/** Blocking instructions **/`
`34`	`34`
`35`	`35`	`void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {`
	`36`	`+ BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));`
`36`	`37`	`GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::User);`
`37`	`38`	`}`
`38`	`39`