summaryrefslogtreecommitdiffstats
path: root/src/filegen.h
diff options
context:
space:
mode:
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;