1 files changed, 5 insertions, 0 deletions
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();