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_dir.c | |
| parent | a6447a48e1e2c7a7c15e8bead720b3a54fc983a6 (diff) | |
Improve Frama-C annotations for a bunch of files
Diffstat (limited to 'src/file_dir.c')
| -rw-r--r-- | src/file_dir.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/file_dir.c b/src/file_dir.c index 387b4e0c..9953959f 100644 --- a/src/file_dir.c +++ b/src/file_dir.c @@ -79,6 +79,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery) @ requires file_recovery->data_check == &data_check_fatdir; @ requires buffer_size >= 2; @ requires valid_data_check_param(buffer, buffer_size, file_recovery); + @ terminates \true; @ ensures valid_data_check_result(\result, file_recovery); @ ensures \result == DC_STOP; @ assigns file_recovery->calculated_file_size; |