summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/pervasive.h10
-rw-r--r--src/sequence/sequence.h175
-rw-r--r--src/sequence/sequence_append.c57
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;
}