summaryrefslogtreecommitdiff
path: root/src/knowledge
diff options
context:
space:
mode:
Diffstat (limited to 'src/knowledge')
-rw-r--r--src/knowledge/knowledge.c21
-rw-r--r--src/knowledge/knowledge.h49
-rw-r--r--src/knowledge/knowledge_finalize.c6
-rw-r--r--src/knowledge/knowledge_get_random_sequence.c9
-rw-r--r--src/knowledge/knowledge_learn_markov_sequence.c10
-rw-r--r--src/knowledge/knowledge_learn_word.c6
-rw-r--r--src/knowledge/knowledge_types.h10
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