summaryrefslogtreecommitdiff
path: root/src/cobs.c
diff options
context:
space:
mode:
authorjaseg <git@jaseg.net>2018-12-17 22:51:47 +0900
committerjaseg <git@jaseg.net>2018-12-17 22:51:47 +0900
commit0f26179409297c921b4b7ffd9d6379bab84f964b (patch)
tree27015b688222d248d23785eac11ab400a332ad0d /src/cobs.c
parent59b01a744279b1287db1fb8d73ab69450758b1fb (diff)
downloadsecure-hid-0f26179409297c921b4b7ffd9d6379bab84f964b.tar.gz
secure-hid-0f26179409297c921b4b7ffd9d6379bab84f964b.tar.bz2
secure-hid-0f26179409297c921b4b7ffd9d6379bab84f964b.zip
Document function specs some more
Diffstat (limited to 'src/cobs.c')
-rw-r--r--src/cobs.c1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/cobs.c b/src/cobs.c
index d3889c3..19dcad2 100644
--- a/src/cobs.c
+++ b/src/cobs.c
@@ -73,7 +73,6 @@ ssize_t cobs_encode(char *dst, size_t dstlen, char *src, size_t srclen) {
}
/*@ requires \valid_read(src + (0..srclen-1));
- @ requires srclen < 1000000-2;
@*/
#ifndef VERIFICATION
int cobs_encode_incremental(void *f, int (*output)(void *f, unsigned char c), unsigned char *src, size_t srclen) {