Seems to work reasonably well.code-improvements

7 files changed, 95 insertions, 16 deletions

diff --git a/src/knowledge/knowledge.c b/src/knowledge/knowledge.c
index e7d1cd9..ec6e098 100644
--- a/src/knowledge/knowledge.c
+++ b/src/knowledge/knowledge.c
@@ -23,14 +23,19 @@ int ZoO_knowledge_initialize (struct ZoO_knowledge k [const restrict static 1])
    k->sequences_length = 0;
    k->sequences_sorted = (ZoO_index *) NULL;
 
+#ifndef ZoO_RUNNING_FRAMA_C
    error = pthread_mutex_init(&(k->mutex), (const pthread_mutexattr_t *) NULL);
+#else
+   k->mutex = 1;
+   error = 0;
+#endif
 
    if (error != 0)
    {
-      fprintf
+      ZoO_FATAL
       (
          stderr,
-         "[F] Unable to initialize knowledge mutex: %s.\n",
+         "Unable to initialize knowledge mutex: %s.",
          strerror(error)
       );
 
@@ -78,7 +83,13 @@ int ZoO_knowledge_lock_access
 {
    int err;
 
+#ifndef ZoO_RUNNING_FRAMA_C
    err = pthread_mutex_lock(&(k->mutex));
+#else
+   /*@ assert (k->mutex == 1); @*/
+   k->mutex = 0;
+   err = 0;
+#endif
 
    if (err != 0)
    {
@@ -103,7 +114,13 @@ void ZoO_knowledge_unlock_access
 {
    int err;
 
+#ifndef ZoO_RUNNING_FRAMA_C
    err = pthread_mutex_unlock(&(k->mutex));
+#else
+   /*@ assert (k->mutex == 0); @*/
+   k->mutex = 1;
+   err = 0;
+#endif
 
    if (err != 0)
    {
diff --git a/src/knowledge/knowledge.h b/src/knowledge/knowledge.h
index 876dbe4..9d028ab 100644
--- a/src/knowledge/knowledge.h
+++ b/src/knowledge/knowledge.h
@@ -8,18 +8,67 @@
 
 #include "knowledge_types.h"
 
+/*@
+   requires \valid(k);
+   requires \separated(k, io);
+
+// Do not use if lock is already yours.
+   requires (k->mutex == 1);
+
+// Returns zero on success, -1 on failure.
+   assigns \result;
+   ensures ((\result == 0) || (\result == -1));
+
+// On success, lock is acquired.
+   ensures ((\result == 0) ==> (k->mutex == 0));
+
+// Changes the status of the lock.
+   assigns (k->mutex);
+@*/
 int ZoO_knowledge_lock_access
 (
    struct ZoO_knowledge k [const restrict static 1],
    FILE io [const restrict static 1]
 );
 
+/*@
+   requires \valid(k);
+   requires \separated(k, io);
+
+// Do not use if lock is not yours.
+   requires (k->mutex == 0);
+
+// Lock is released.
+   ensures (k->mutex == 1);
+
+// Changes the status of the lock.
+   assigns (k->mutex);
+@*/
 void ZoO_knowledge_unlock_access
 (
    struct ZoO_knowledge k [const restrict static 1],
    FILE io [const restrict static 1]
 );
 
+/*@
+   requires (\block_length(k) >= 1);
+
+// Returns zero on success, -1 on failure.
+   assigns \result;
+   ensures ((\result == 0) || (\result == -1));
+
+// On success, all fields of {*k} are set.
+   ensures ((\result == 0) ==> \valid(k));
+
+// On success, the two reserved words are learnt.
+   ensures ((\result == 0) ==> (k->words_length == 2));
+
+// On success, the mutex is initialized and unlocked.
+   ensures ((\result == 0) ==> (k->mutex == 1));
+
+// At least some fields of k are set in any case.
+   assigns (*k);
+@*/
 int ZoO_knowledge_initialize (struct ZoO_knowledge k [const restrict static 1]);
 
 void ZoO_knowledge_finalize (struct ZoO_knowledge k [const restrict static 1]);
diff --git a/src/knowledge/knowledge_finalize.c b/src/knowledge/knowledge_finalize.c
index 37548d4..cec0ff6 100644
--- a/src/knowledge/knowledge_finalize.c
+++ b/src/knowledge/knowledge_finalize.c
@@ -2,6 +2,9 @@
 
 #include "knowledge.h"
 
+/*@
+   requires \valid(sd);
+@*/
 static void knowledge_sequence_data_finalize
 (
    struct ZoO_knowledge_sequence_data sd [const restrict static 1]
@@ -27,7 +30,6 @@ static void knowledge_sequence_collection_finalize
 {
    ZoO_index i;
 
-
    for (i = 0; i < c->sequences_ref_length; ++i)
    {
       knowledge_sequence_data_finalize(c->sequences_ref + i);
@@ -36,12 +38,14 @@ static void knowledge_sequence_collection_finalize
    if (c->sequences_ref != (struct ZoO_knowledge_sequence_data *) NULL)
    {
       free((void *) c->sequences_ref);
+
       c->sequences_ref = (struct ZoO_knowledge_sequence_data *) NULL;
    }
 
    if (c->sequences_ref_sorted != (ZoO_index *) NULL)
    {
       free((void *) c->sequences_ref_sorted);
+
       c->sequences_ref_sorted = (ZoO_index *) NULL;
    }
 
diff --git a/src/knowledge/knowledge_get_random_sequence.c b/src/knowledge/knowledge_get_random_sequence.c
index 92800a4..39fbd50 100644
--- a/src/knowledge/knowledge_get_random_sequence.c
+++ b/src/knowledge/knowledge_get_random_sequence.c
@@ -68,8 +68,13 @@ int ZoO_knowledge_copy_random_swt_sequence
       ) < 0
    )
    {
-      /* TODO: Err message. */
-
+      ZoO_S_PROG_ERROR
+      (
+         io,
+         "Knowledge inconsistency; there are no acceptable markov sequences "
+         "linked to a word that has been picked as being an acceptable pillar."
+      )
+   ;
       return -1;
    }
 
diff --git a/src/knowledge/knowledge_learn_markov_sequence.c b/src/knowledge/knowledge_learn_markov_sequence.c
index 54357c0..ce38b06 100644
--- a/src/knowledge/knowledge_learn_markov_sequence.c
+++ b/src/knowledge/knowledge_learn_markov_sequence.c
@@ -50,7 +50,7 @@ static int reallocate_sequences_list
       ZoO_S_ERROR
       (
          io,
-         "Unable to store the size of the sequences list, as it would overflow"
+         "Unable to store the size of the sequences list, as it would overflow "
          "size_t variables."
       );
 
@@ -93,8 +93,8 @@ static int reallocate_sequences_sorted_list
       ZoO_S_ERROR
       (
          io,
-         "Unable to store the size of the sorted sequences list, as it would"
-         " overflow size_t variables."
+         "Unable to store the size of the sorted sequences list, as it would "
+         "overflow size_t variables."
       );
 
       return -1;
@@ -112,8 +112,8 @@ static int reallocate_sequences_sorted_list
       ZoO_S_ERROR
       (
          io,
-         "Unable to allocate the memory required for the new sorted sequences"
-         " list."
+         "Unable to allocate the memory required for the new sorted sequences "
+         "list."
       );
 
       return -1;
diff --git a/src/knowledge/knowledge_learn_word.c b/src/knowledge/knowledge_learn_word.c
index 605af8e..8af3ef0 100644
--- a/src/knowledge/knowledge_learn_word.c
+++ b/src/knowledge/knowledge_learn_word.c
@@ -87,7 +87,7 @@ static int reallocate_words_list
       ZoO_S_ERROR
       (
          io,
-         "Unable to store the size of the words list, as it would overflow"
+         "Unable to store the size of the words list, as it would overflow "
          "size_t variables."
       );
 
@@ -134,8 +134,8 @@ static int reallocate_words_sorted_list
    {
       ZoO_S_ERROR
       (
-         "Unable to store the size of the sorted words list, as it would"
-         " overflow size_t variables."
+         "Unable to store the size of the sorted words list, as it would "
+         "overflow size_t variables."
       );
 
       return -1;
diff --git a/src/knowledge/knowledge_types.h b/src/knowledge/knowledge_types.h
index 53330ce..a314927 100644
--- a/src/knowledge/knowledge_types.h
+++ b/src/knowledge/knowledge_types.h
@@ -44,15 +44,19 @@ struct ZoO_knowledge_word
 
 struct ZoO_knowledge
 {
+#ifndef ZoO_RUNNING_FRAMA_C
+   pthread_mutex_t mutex;
+#else
+   int mutex;
+#endif
+
    struct ZoO_knowledge_word * words;
    ZoO_index words_length;
    ZoO_index * words_sorted;
+
    ZoO_index ** sequences;
    ZoO_index sequences_length;
    ZoO_index * sequences_sorted;
-#ifndef ZoO_RUNNING_FRAMA_C
-   pthread_mutex_t mutex;
-#endif
 };
 
 #endif