diff options
author | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:00:52 +0100 |
---|---|---|
committer | Christophe Grenier <grenier@cgsecurity.org> | 2023-12-27 11:00:52 +0100 |
commit | 84535f854742da2521f9b99caf46c7220b9aa470 (patch) | |
tree | 31d6efbc810124437f9eb5f2c6ed2446c9606c39 /src | |
parent | 133a1bf80a313cd82a432c4a0e91f5ee7d05237b (diff) |
src/fidentify.c: more frama-c annotations
Diffstat (limited to 'src')
-rw-r--r-- | src/fidentify.c | 2 |
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); */ } |