diff options
| author | Christophe Grenier <[email protected]> | 2024-01-01 20:08:58 +0100 |
|---|---|---|
| committer | Christophe Grenier <[email protected]> | 2024-01-01 20:08:58 +0100 |
| commit | e45f0d5b6951de6127e5130d0522f07c7fe638c9 (patch) | |
| tree | 88774dedefcc61a9d14a386514fa8ec1309b4bbe /src/file_vault.c | |
| parent | a6447a48e1e2c7a7c15e8bead720b3a54fc983a6 (diff) | |
Improve Frama-C annotations for a bunch of files
Diffstat (limited to 'src/file_vault.c')
| -rw-r--r-- | src/file_vault.c | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/file_vault.c b/src/file_vault.c index 4b659731..eafa692e 100644 --- a/src/file_vault.c +++ b/src/file_vault.c @@ -53,6 +53,7 @@ const file_hint_t file_hint_vault = { @ requires buffer_size >= 2*29; @ requires file_recovery->data_check==&data_check_vault; @ requires valid_data_check_param(buffer, buffer_size, file_recovery); + @ terminates \true; @ ensures valid_data_check_result(\result, file_recovery); @ assigns file_recovery->calculated_file_size; @*/ @@ -61,7 +62,10 @@ static data_check_t data_check_vault(const unsigned char *buffer, const unsigned unsigned int i; /*@ assert file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */ /*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */ - /*@ loop assigns i, file_recovery->calculated_file_size; */ + /*@ + @ loop assigns i, file_recovery->calculated_file_size; + @ loop variant buffer_size - (i + 29); + @*/ for(i = (buffer_size / 2) - 28; i + 29 <= buffer_size; i++) { if(buffer[i] == '-' && buffer[i + 5] == '-' && buffer[i + 10] == '-' && buffer[i + 15] == '-' && buffer[i + 28] == '\0') @@ -77,6 +81,7 @@ static data_check_t data_check_vault(const unsigned char *buffer, const unsigned /*@ @ requires separation: \separated(&file_hint_vault, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); + @ terminates \true; @ ensures valid_header_check_result(\result, file_recovery_new); @ assigns *file_recovery_new; @*/ |