From 219bd3a3aeb77e56c1d1c2db2c9dd2ddb26a39f8 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sat, 4 Sep 2021 18:44:35 +0200 Subject: [PATCH] src/file_riff.h: improve Frama-C annotations --- src/file_riff.h | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/file_riff.h b/src/file_riff.h index b0aa48d9..a9e4c1c6 100644 --- a/src/file_riff.h +++ b/src/file_riff.h @@ -26,14 +26,9 @@ extern "C" { #endif /*@ - @ requires buffer_size > 0; - @ requires (buffer_size&1)==0; - @ requires \valid_read(buffer+(0..buffer_size-1)); - @ requires \valid(file_recovery); @ requires file_recovery->data_check==&data_check_avi_stream; - @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; - @ requires \separated(buffer, file_recovery); - @ ensures \result == DC_CONTINUE || \result == DC_STOP; + @ requires valid_data_check_param(buffer, buffer_size, file_recovery); + @ ensures valid_data_check_result(\result, file_recovery); @ assigns file_recovery->calculated_file_size; @*/ data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);