X-Git-Url: https://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu-controldataflow%2Furcu.spin;h=3956d75ecd20567f2b8fe1064c0f44bf2070f0b3;hp=b3290589324e50904d045b54deeb0c95970c946f;hb=abbe7e27151039f5f56b7130f0043f703862e99c;hpb=6af482a9e24a5ee17eef220b25a050be5df8aa39

diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin
index b329058..3956d75 100644
--- a/formal-model/urcu-controldataflow/urcu.spin
+++ b/formal-model/urcu-controldataflow/urcu.spin
@@ -349,7 +349,7 @@ DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
 /* RCU pointer */
 DECLARE_CACHED_VAR(byte, rcu_ptr);
 /* RCU data */
-DECLARE_CACHED_VAR(byte, rcu_data[2]);
+DECLARE_CACHED_VAR(byte, rcu_data[SLAB_SIZE]);
 
 byte ptr_read[NR_READERS];
 byte data_read[NR_READERS];