diff options
| author | jaseg <git@jaseg.net> | 2018-12-17 13:38:39 +0900 |
|---|---|---|
| committer | jaseg <git@jaseg.net> | 2018-12-17 13:38:39 +0900 |
| commit | 447d084d79cc139d0aaa4433148cc7c310bfaf0d (patch) | |
| tree | 4fce2f3db95c5dd62d4e9342c553b74badb822f4 /include | |
| parent | 40e9fb8153a218a243cff749d7d0b4e82d70ae94 (diff) | |
| download | secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.tar.gz secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.tar.bz2 secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.zip | |
First steps to prove cobs decoder
Diffstat (limited to 'include')
| -rw-r--r-- | include/cobs.h | 6 |
1 files changed, 5 insertions, 1 deletions
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__ |