1 files changed, 7 insertions, 2 deletions
diff --git a/src/core/index.h b/src/core/index.h
index 1417662..eb3c471 100644
--- a/src/core/index.h
+++ b/src/core/index.h
@@ -6,14 +6,19 @@
 /*
  * Returns a random ZoO_index.
  */
+/*@
+   ensures (\result <= ZoO_INDEX_MAX);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random (void);
 
 /*
  * Returns a random ZoO_index, included in [0, limit]
  */
 /*@
- @ ensures (\result <= limit);
- @*/
+   ensures (\result <= limit);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random_up_to (const ZoO_index limit);
 
 #endif