Execute sig handler unconditionnally

[urcu.git] / formal-model / urcu / urcu.spin

diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index d1aff29fee663d28249a9e608992781741d4e169..630971f0a280827157bfb19937d7bdbd1d181814 100644 (file)
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -264,6 +264,16 @@ inline wait_init_done()
 
 #ifdef TEST_SIGNAL
 
+inline wait_for_sighand_exec()
+{
+       sighand_exec = 0;
+       do
+       :: sighand_exec == 0 -> skip;
+       :: else -> break;
+       od;
+}
+
+#ifdef TOO_BIG_STATE_SPACE
 inline wait_for_sighand_exec()
 {
        sighand_exec = 0;
@@ -277,6 +287,7 @@ inline wait_for_sighand_exec()
                fi;
        od;
 }
+#endif
 
 #else