summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2023-12-27 11:00:52 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2023-12-27 11:00:52 +0100
commit84535f854742da2521f9b99caf46c7220b9aa470 (patch)
tree31d6efbc810124437f9eb5f2c6ed2446c9606c39 /src
parent133a1bf80a313cd82a432c4a0e91f5ee7d05237b (diff)
src/fidentify.c: more frama-c annotations
Diffstat (limited to 'src')
-rw-r--r--src/fidentify.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/fidentify.c b/src/fidentify.c
index 259cf361..68403e36 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -141,6 +141,7 @@ static data_check_t data_check_aux(file_recovery_t *file_recovery, const unsigne
@ loop assigns i, file_recovery->file_size;
@ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@ loop assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
+ @ loop variant lu - i;
@*/
for(i=0; i<lu; i+=blocksize)
{
@@ -168,6 +169,7 @@ static data_check_t data_check_aux(file_recovery_t *file_recovery, const unsigne
/*@ assert valid_file_recovery(file_recovery); */
return DC_STOP;
}
+ /*@ assert valid_file_recovery(file_recovery); */
memcpy(buffer_start, &buffer_start[READ_SIZE], blocksize);
/*@ assert valid_file_recovery(file_recovery); */
}