From 77816b359d111bbf88cb532394347126cfcb8c85 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 14 Feb 2021 17:26:25 +0100 Subject: [PATCH] src/file_cwk.c: add frama-c annotations --- src/file_cwk.c | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/file_cwk.c b/src/file_cwk.c index 6b9f1b2b..6838789d 100644 --- a/src/file_cwk.c +++ b/src/file_cwk.c @@ -32,9 +32,8 @@ #include "filegen.h" #include "common.h" +/*@ requires \valid(file_stat); */ static void register_header_check_cwk(file_stat_t *file_stat); -static int header_check_cwk(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 void file_check_cwk(file_recovery_t *file_recovery); const file_hint_t file_hint_cwk= { .extension="cwk", @@ -65,12 +64,35 @@ struct cwk_header uint16_t inner_width; } __attribute__ ((gcc_struct, __packed__)); +/*@ + @ requires valid_file_recovery(file_recovery); + @ requires \valid(file_recovery->handle); + @ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source); + @ requires \initialized(&file_recovery->time); + @ + @ requires file_recovery->file_check == &file_check_cwk; + @ assigns *file_recovery->handle, errno, file_recovery->file_size; + @ assigns Frama_C_entropy_source; + @ + @ ensures \valid(file_recovery->handle); + @*/ static void file_check_cwk(file_recovery_t *file_recovery) { const unsigned char cwk_footer[4]= {0xf0, 0xf1, 0xf2, 0xf3}; file_search_footer(file_recovery, cwk_footer, sizeof(cwk_footer), 4); } +/*@ + @ requires buffer_size >= sizeof(struct cwk_header); + @ 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_cwk, 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_cwk(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 struct cwk_header *cwk=(const struct cwk_header *)buffer;