From a9d7aacefa0405920f1b8655935febc6b3caf5fe Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 14 Feb 2021 21:26:32 +0100 Subject: [PATCH] src/file_dpx.c: add frama-c annotations --- src/file_dpx.c | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/file_dpx.c b/src/file_dpx.c index 89368cc3..ca0ab0af 100644 --- a/src/file_dpx.c +++ b/src/file_dpx.c @@ -35,6 +35,7 @@ #include "filegen.h" #include "common.h" +/*@ requires \valid(file_stat); */ static void register_header_check_dpx(file_stat_t *file_stat); const file_hint_t file_hint_dpx= { @@ -66,17 +67,29 @@ struct header_dpx char Reserved[104]; /* reserved field TBD (need to pad) */ } __attribute__ ((gcc_struct, __packed__)); +/*@ + @ requires buffer_size >= sizeof(struct header_dpx); + @ 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_dpx, buffer+(..), file_recovery, file_recovery_new); + @ assigns *file_recovery_new; + @ ensures \result == 0 || \result == 1; + @ ensures \result!=0 ==> valid_file_recovery(file_recovery_new); + @*/ static int header_check_dpx(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) { static const unsigned char ver10[8]= {'V', '1', '.', '0', 0x00, 0x00, 0x00, 0x00}; const struct header_dpx *dpx=(const struct header_dpx *)buffer; + const unsigned int file_size=be32(dpx->file_size); if(memcmp(dpx->vers, ver10, sizeof(ver10))==0) { - if(be32(dpx->file_size) < 19) + if(file_size < sizeof(struct header_dpx)) return 0; reset_file_recovery(file_recovery_new); file_recovery_new->extension=file_hint_dpx.extension; - file_recovery_new->calculated_file_size=be32(dpx->file_size); + file_recovery_new->calculated_file_size=file_size; file_recovery_new->data_check=&data_check_size; file_recovery_new->file_check=&file_check_size; file_recovery_new->time=get_time_from_YYYY_MM_DD_HH_MM_SS(dpx->create_time); @@ -88,6 +101,8 @@ static int header_check_dpx(const unsigned char *buffer, const unsigned int buff static void register_header_check_dpx(file_stat_t *file_stat) { register_header_check(0, "SDPX", 4, &header_check_dpx, file_stat); +#ifndef __FRAMAC__ register_header_check(0, "XPDS", 4, &header_check_dpx, file_stat); +#endif } #endif