projects
/
urcu.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
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
This page took
0.023448 seconds
and
4
git commands to generate.