From 0f26179409297c921b4b7ffd9d6379bab84f964b Mon Sep 17 00:00:00 2001 From: jaseg Date: Mon, 17 Dec 2018 22:51:47 +0900 Subject: Document function specs some more --- src/cobs.c | 1 - 1 file changed, 1 deletion(-) (limited to 'src/cobs.c') 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) { -- cgit