summaryrefslogtreecommitdiffstats
path: root/src/file_mov.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_mov.c')
-rw-r--r--src/file_mov.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/file_mov.c b/src/file_mov.c
index 2246cd7..b330395 100644
--- a/src/file_mov.c
+++ b/src/file_mov.c
@@ -103,6 +103,7 @@ static void file_rename_mov(file_recovery_t *file_recovery)
/*@
@ requires buffer_size >= 16;
+ @ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_mov;