From 447d084d79cc139d0aaa4433148cc7c310bfaf0d Mon Sep 17 00:00:00 2001 From: jaseg Date: Mon, 17 Dec 2018 13:38:39 +0900 Subject: First steps to prove cobs decoder --- include/cobs.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'include/cobs.h') diff --git a/include/cobs.h b/include/cobs.h index 6c70c02..1cc2681 100644 --- a/include/cobs.h +++ b/include/cobs.h @@ -17,7 +17,11 @@ ssize_t cobs_decode(char *dst, size_t dstlen, char *src, size_t srclen); int cobs_encode_incremental(void *f, int (*output)(void *, char), char *src, size_t srclen); +/*@ requires \valid(state); + ensures state->p == 0 && state->c == 0; + assigns *state; + @*/ void cobs_decode_incremental_initialize(struct cobs_decode_state *state); -int cobs_decode_incremental(struct cobs_decode_state *state, char *dst, size_t dstlen, char src); +int cobs_decode_incremental(struct cobs_decode_state *state, unsigned char *dst, size_t dstlen, unsigned char src); #endif//__COBS_H__ -- cgit