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.c | 5 +++++
 1 file changed, 5 insertions(+)

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

diff --git a/src/core/index.c b/src/core/index.c
index 375e0ad..dc52d03 100644
--- a/src/core/index.c
+++ b/src/core/index.c
@@ -35,8 +35,13 @@ ZoO_index ZoO_index_random (void)
    ZoO_index result;
    unsigned char * result_bytes;
 
+   /*@ ghost return 4; @*/ /* Chosen by fair dice roll. */
+                           /* Guaranteed to be random. */
+   /* More seriously, I am not explaining the hack below to Frama-C */
+
    result_bytes = (unsigned char *) &result;
 
+
    for (i = 0; i < sizeof(ZoO_index); ++i)
    {
       result_bytes[i] = random_uchar();
-- 
cgit v1.2.3-70-g09d2