summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-02-03 22:20:35 +0100
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-02-03 22:20:35 +0100
commitee26b8ff850add4f83b912635a71dbde06f268d1 (patch)
treeada230a0d34aaf2a0e9fbecadde0bdf0dcdf1da4 /src/sequence/sequence.c
parent1dafef5fdf9d98b38cbe717b8a220d721f0ebea8 (diff)
Continuing Implementation...
Diffstat (limited to 'src/sequence/sequence.c')
-rw-r--r--src/sequence/sequence.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sequence/sequence.c b/src/sequence/sequence.c
index 852b05c..f3c3b46 100644
--- a/src/sequence/sequence.c
+++ b/src/sequence/sequence.c
@@ -75,13 +75,13 @@ static void bypass_redundant_sos
/* See "sequence.h" */
/*@
- \requires
+ requires
(
\valid(sequence_a+ (0 .. sequence_a_length))
|| (sequence_a_length == 0)
);
- \requires
+ requires
(
\valid(sequence_b+ (0 .. sequence_b_length))
|| (sequence_b_length == 0)