summaryrefslogtreecommitdiffstats
path: root/src/file_gpg.c
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:40:59 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:40:59 +0100
commit4df871bf15bd29319eeb127af798ebe13c0ffc5a (patch)
tree57ec4575ad442c76fa61527eccbec11746200716 /src/file_gpg.c
parent9b51c2aeb03fe414b7946043ad39e7ab0b1d0cf9 (diff)
PhotoRec: add a few frama-c annotations, mostly in header_check functions
Diffstat (limited to 'src/file_gpg.c')
-rw-r--r--src/file_gpg.c12
1 files changed, 11 insertions, 1 deletions
diff --git a/src/file_gpg.c b/src/file_gpg.c
index ac700e2..ec9635e 100644
--- a/src/file_gpg.c
+++ b/src/file_gpg.c
@@ -474,8 +474,18 @@ static void file_check_gpg(file_recovery_t *file_recovery)
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
- @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_gpg);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_gpg.extension || file_recovery_new->extension == extension_pgp);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_gpg);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
@*/
static int header_check_gpg(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{