summaryrefslogtreecommitdiffstats
path: root/src/filegen.h
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-01 16:34:38 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-01 16:34:38 +0100
commit611da961b33b7d1d0b68a8d7f87437417055dab5 (patch)
treedacb63b764eb983bb828d7e3eb8aca788784aec2 /src/filegen.h
parentf5f3120cfa5c60f8921a1244accf8026e0f1cd8c (diff)
add a few frama-c annotations
Diffstat (limited to 'src/filegen.h')
-rw-r--r--src/filegen.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/filegen.h b/src/filegen.h
index 7a1807b..a7ebde4 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -144,7 +144,8 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
/*@
- @ requires buffer_size > 0;
+ @ requires buffer_size >= 2;
+ @ requires (buffer_size&1)==0;
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check == &data_check_size;