From 1373211465c34015ee900e097aa87fbffb401187 Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Sun, 29 Jan 2017 19:54:26 +0100
Subject: Trying out ACSL, continuing implementation.

---
 src/core/index.h | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'src/core/index.h')

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
-- 
cgit v1.2.3-70-g09d2