Made Frama-C give up.

It validates (*sequence_length == (\old(*sequence_length) + 1))
regardless of the addition of an "*sequence_length -= 1;" in the code.

3 files changed, 159 insertions, 83 deletions

diff --git a/src/pervasive.h b/src/pervasive.h
index e5cda3b..7359a3d 100644
--- a/src/pervasive.h
+++ b/src/pervasive.h
@@ -6,20 +6,14 @@
 #define ZoO_SERVER_VERSION    1
 #define ZoO_PROTOCOL_VERSION  1
 
+#define ZoO_RUNNING_FRAMA_C   1
+
 #define ZoO_DEBUG_ALL 1
 
 #ifndef ZoO_DEBUG_ALL
    #define ZoO_DEBUG_ALL 0
 #endif
 
-#ifndef ZoO_NETWORK_TIMEOUT
-   #define ZoO_NETWORK_TIMEOUT            200
-#endif
-
-#ifndef ZoO_MAX_REPLY_WORDS
-   #define ZoO_MAX_REPLY_WORDS            64
-#endif
-
 #define ZoO__TO_STRING(x) #x
 #define ZoO_TO_STRING(x) ZoO__TO_STRING(x)
 #define ZoO_ISOLATE(a) do {a} while (0)
diff --git a/src/sequence/sequence.h b/src/sequence/sequence.h
index d1ac16f..d9cbf86 100644
--- a/src/sequence/sequence.h
+++ b/src/sequence/sequence.h
@@ -18,43 +18,52 @@
    requires \valid(*sequence);
    requires \valid(sequence_capacity);
    requires \valid(io);
-   requires ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
-   requires (*sequence_capacity >= 0);
-   requires (*sequence_capacity <= SIZE_MAX);
+
    requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
-   requires \separated(sequence, sequence_capacity, io);
+   requires ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
 
-   ensures
-   (
-      (
-         (\result >= 0)
-         && (*sequence_capacity >= sequence_required_capacity)
-         && ((*sequence_capacity * sizeof(ZoO_index)) <= SIZE_MAX)
-      )
-      || (\result < 0)
-   );
+   requires \separated(sequence, *sequence, sequence_capacity, io);
 
-   behavior successful_reallocation:
-      assigns (*sequence);
-      assigns (*sequence_capacity);
+   ensures \separated(sequence, *sequence, sequence_capacity, io);
+   ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures \valid(sequence);
+   ensures \valid(*sequence);
+   ensures \valid(sequence_capacity);
+   ensures \valid(io);
 
-      ensures (\result > 0);
-      ensures ((*sequence_capacity) == sequence_required_capacity);
-      ensures \valid(sequence);
+   assigns (*sequence);
+   assigns (*sequence_capacity);
 
-   behavior already_done:
-      assigns \nothing;
+   ensures ((\result == 1) || (\result == 0) || (\result == -1));
 
-      ensures (\result == 0);
-      ensures ((*sequence_capacity) >= sequence_required_capacity);
+   ensures
+      (
+         (\result == 1) ==>
+            ((*sequence_capacity) == sequence_required_capacity)
+      );
 
-   behavior failure:
-      assigns \nothing;
+   ensures
+      (
+         (\result == 1) ==>
+            ((*sequence_capacity) > \old(*sequence_capacity))
+      );
 
-      ensures (\result < 0);
+   ensures ((\result == -1) ==> ((*sequence) == \old(*sequence)));
 
-   complete behaviors;
-   disjoint behaviors;
+   ensures
+      (
+         (\result == -1) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
+
+   ensures ((\result == 0) ==> ((*sequence) == \old(*sequence)));
+
+   ensures
+      (
+         (\result == 0) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
 @*/
 int ZoO_sequence_ensure_capacity
 (
@@ -109,30 +118,58 @@ int ZoO_sequence_create_from
 );
 
 /*@
+   requires \valid(sequence);
+   requires \valid(*sequence);
+   requires \valid(sequence_capacity);
    requires \valid(sequence_length);
    requires \valid(io);
    requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
    requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
-   requires \separated(sequence, sequence_capacity, sequence_length, io);
+   requires \separated(sequence, sequence, sequence_capacity, sequence_length, io);
 
-   behavior success:
-      assigns (*sequence_length);
-      assigns (*sequence[0]);
-      assigns (*sequence_capacity);
+   assigns (*sequence_length);
+   assigns (*sequence[0]);
+   assigns (*sequence_capacity);
 
-      ensures (\result >= 0);
-      ensures ((*sequence_length > \old(*sequence_length)));
+   ensures \valid(sequence);
+   ensures \valid(sequence_capacity);
+   ensures \valid(sequence_length);
+   ensures \valid(io);
+   ensures (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures \separated(sequence, *sequence, sequence_capacity, sequence_length, io);
 
-   behavior could_not_increase_length:
-      ensures (\result == -1);
+   ensures ((\result == 0) || (\result == -1));
 
-      assigns (*sequence_length);
+   ensures
+   (
+      (\result == 0) ==>
+         (*sequence_length == (\old(*sequence_length) + 1))
+   );
 
-   behavior could_not_reallocate:
-      ensures (\result < -1);
+   ensures
+      (
+         (\result == 0) ==>
+            ((*sequence_capacity) >= \old(*sequence_capacity))
+      );
+
+   ensures ((\result == 0) ==> (*sequence_length > \old(*sequence_length)));
+
+   ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+   ensures ((\result == -1) ==> ((*sequence[0]) == \old(*sequence[0])));
+   ensures
+      (
+         (\result == -1) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
+
+   ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+   ensures
+      (
+         (\result == -1) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
 
-   complete behaviors;
-   disjoint behaviors;
 @*/
 int ZoO_sequence_append_left
 (
@@ -144,32 +181,58 @@ int ZoO_sequence_append_left
 );
 
 /*@
+   requires \valid(sequence);
    requires \valid(*sequence);
    requires \valid(sequence_capacity);
    requires \valid(sequence_length);
    requires \valid(io);
    requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
    requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
-   requires \separated(sequence, sequence_capacity, sequence_length, io);
+   requires \separated(sequence, sequence, sequence_capacity, sequence_length, io);
+
+   assigns (*sequence_length);
+   assigns (*sequence[0]);
+   assigns (*sequence_capacity);
 
-   behavior success:
-      assigns (*sequence_length);
-      assigns (*sequence);
-      assigns (*sequence_capacity);
+   ensures \valid(sequence);
+   ensures \valid(sequence_capacity);
+   ensures \valid(sequence_length);
+   ensures \valid(io);
+   ensures (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures \separated(sequence, *sequence, sequence_capacity, sequence_length, io);
 
-      ensures (\result >= 0);
-      ensures ((*sequence_length > \old(*sequence_length)));
+   ensures ((\result == 0) || (\result == -1));
 
-   behavior could_not_increase_length:
-      ensures (\result == -1);
+   ensures
+   (
+      (\result == 0) ==>
+         (*sequence_length == (\old(*sequence_length) + 1))
+   );
+
+   ensures
+      (
+         (\result == 0) ==>
+            ((*sequence_capacity) >= \old(*sequence_capacity))
+      );
 
-      assigns (*sequence_length);
+   ensures ((\result == 0) ==> (*sequence_length > \old(*sequence_length)));
 
-   behavior could_not_reallocate:
-      ensures (\result < -1);
+   ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+   ensures ((\result == -1) ==> ((*sequence[0]) == \old(*sequence[0])));
+   ensures
+      (
+         (\result == -1) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
+
+   ensures ((\result == -1) ==> ((*sequence_length) == \old(*sequence_length)));
+   ensures
+      (
+         (\result == -1) ==>
+            ((*sequence_capacity) == \old(*sequence_capacity))
+      );
 
-   complete behaviors;
-   disjoint behaviors;
 @*/
 int ZoO_sequence_append_right
 (
diff --git a/src/sequence/sequence_append.c b/src/sequence/sequence_append.c
index a119d8b..7eaa22b 100644
--- a/src/sequence/sequence_append.c
+++ b/src/sequence/sequence_append.c
@@ -16,28 +16,37 @@
 /*@
    requires \valid(required_capacity);
    requires \valid(io);
-   requires (*required_capacity >= 0);
-   requires (*required_capacity <= SIZE_MAX);
    requires \separated(required_capacity, io);
 
    assigns \result;
 
-   ensures (*required_capacity >= 0);
+   assigns (*required_capacity);
 
-   behavior success:
-      assigns (*required_capacity);
+   ensures ((\result == 0) || (\result == -1));
 
-      ensures (\result >= 0);
-      ensures ((*required_capacity) == (\old(*required_capacity) + 1));
-      ensures (((*required_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   ensures \valid(required_capacity);
+   ensures \valid(io);
 
-   behavior failure:
-      assigns \nothing;
+   ensures \separated(required_capacity, io);
 
-      ensures (\result < 0);
+   ensures
+      (
+         (\result == 0) <==>
+               ((*required_capacity) == (\old(*required_capacity) + 1))
+      );
+
+   ensures
+      (
+         (\result == 0) ==>
+            ((*required_capacity) * sizeof(ZoO_index)) <= SIZE_MAX
+      );
+
+   ensures
+      (
+         (\result == -1) <==>
+            ((*required_capacity) == \old(*required_capacity))
+      );
 
-   complete behaviors;
-   disjoint behaviors;
 @*/
 static int increment_required_capacity
 (
@@ -52,13 +61,15 @@ static int increment_required_capacity
    )
    {
       /*@ assert \valid(io); @*/
-      /*@ ghost return -1; @*/
+
+      #ifndef ZoO_RUNNING_FRAMA_C
       ZoO_S_ERROR
       (
          io,
          "Sequence capacity increment aborted, as the new size would not fit"
          " in a size_t variable."
       );
+      #endif
 
       return -1;
    }
@@ -86,6 +97,7 @@ int ZoO_sequence_ensure_capacity
 {
    ZoO_index * new_sequence;
 
+   /*@ assert \valid(sequence_capacity); @*/
    if (sequence_required_capacity <= *sequence_capacity)
    {
       return 0;
@@ -100,7 +112,6 @@ int ZoO_sequence_ensure_capacity
    @*/
    /*@ assert \valid(sequence); @*/
    /*@ assert \valid(*sequence); @*/
-
    new_sequence =
       (ZoO_index *) realloc
       (
@@ -111,13 +122,14 @@ int ZoO_sequence_ensure_capacity
    if (new_sequence == (ZoO_index *) NULL)
    {
       /*@ assert \valid(io); @*/
-      /*@ ghost return -1; @*/
 
+      #ifndef ZoO_RUNNING_FRAMA_C
       ZoO_S_ERROR
       (
          io,
          "Unable to reallocate memory to match sequence's required size."
       );
+      #endif
 
       return -1;
    }
@@ -145,7 +157,6 @@ int ZoO_sequence_append_left
    /*@ assert (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX); @*/
    if
    (
-      /* Appears to make Frama-C forget everything about *sequence_length. */
       ZoO_sequence_ensure_capacity
       (
          sequence,
@@ -155,20 +166,25 @@ int ZoO_sequence_append_left
       ) < 0
    )
    {
-      return -2;
+      *sequence_length -= 1;
+
+      return -1;
    }
+
    /*@ assert *sequence_length >= 0; @*/
 
    if (*sequence_length > 1)
    {
       /*@ assert(((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX); @*/
 
+      #ifndef ZoO_RUNNING_FRAMA_C
       memmove
       (
          (void *) (*sequence + 1),
          (const void *) sequence,
          (((*sequence_length) - 1) * sizeof(ZoO_index))
       );
+      #endif
    }
 
    (*sequence)[0] = word_id;
@@ -190,7 +206,8 @@ int ZoO_sequence_append_right
       return -1;
    }
 
-   /*@ assert ((*sequence_length * sizeof(ZoO_index)) < SIZE_MAX); @*/
+   /*@ assert ((*sequence_length * sizeof(ZoO_index)) <= SIZE_MAX); @*/
+
    if
    (
       ZoO_sequence_ensure_capacity
@@ -202,6 +219,8 @@ int ZoO_sequence_append_right
       ) < 0
    )
    {
+      *sequence_length -= 1;
+
       return -1;
    }