summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2021-09-04 18:44:35 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2021-09-04 18:44:35 +0200
commit219bd3a3aeb77e56c1d1c2db2c9dd2ddb26a39f8 (patch)
tree6c31d8bc34c6590c24dfb88b7e5fe2d514cd0a11
parent5f1002487df106901714dadaceb7ef44b1942048 (diff)
src/file_riff.h: improve Frama-C annotationsHEADmaster
-rw-r--r--src/file_riff.h9
1 files changed, 2 insertions, 7 deletions
diff --git a/src/file_riff.h b/src/file_riff.h
index b0aa48d..a9e4c1c 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);