From 1406dfe5924fdd469ad1b19c6ee103c03465ce1c Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Tue, 27 Jul 2021 21:21:12 +0200 Subject: [PATCH] src/file_wdp.c: improve Frama-C annotations src/file_tiff.h: fix annotation --- src/file_tiff.h | 10 ++++++---- src/file_wdp.c | 11 +++-------- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/src/file_tiff.h b/src/file_tiff.h index 12df8161..ccc22e56 100644 --- a/src/file_tiff.h +++ b/src/file_tiff.h @@ -101,11 +101,13 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns @ requires fr->file_check==&file_check_tiff_le; @ requires valid_file_check_param(fr); @ ensures valid_file_check_result(fr); - @ assigns errno; - @ assigns fr->file_size; - @ assigns *fr->handle; - @ assigns Frama_C_entropy_source; @*/ +/*X FIXME: parse_strip_le calls MALLOC() + X assigns errno; + X assigns fr->file_size; + X assigns *fr->handle; + X assigns Frama_C_entropy_source; + X*/ void file_check_tiff_le(file_recovery_t *fr); #endif diff --git a/src/file_wdp.c b/src/file_wdp.c index 7beb72d7..63c7f14e 100644 --- a/src/file_wdp.c +++ b/src/file_wdp.c @@ -33,9 +33,8 @@ #include "file_tiff.h" #include "common.h" -/*@ requires \valid(file_stat); */ +/*@ requires valid_register_header_check(file_stat); */ static void register_header_check_wdp(file_stat_t *file_stat); -static int header_check_wdp(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); const file_hint_t file_hint_wdp = { .extension = "wdp", @@ -48,13 +47,9 @@ const file_hint_t file_hint_wdp = { /*@ @ requires buffer_size >= sizeof(TIFFHeader); - @ requires \valid_read(buffer+(0..buffer_size-1)); - @ requires valid_file_recovery(file_recovery); - @ requires \valid(file_recovery_new); - @ requires file_recovery_new->blocksize > 0; @ requires separation: \separated(&file_hint_wdp, buffer+(..), file_recovery, file_recovery_new); - @ ensures \result == 0 || \result == 1; - @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); + @ ensures valid_header_check_result(\result, file_recovery_new); @ assigns *file_recovery_new; @*/ static int header_check_wdp(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)