summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-11-17 17:59:26 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-11-17 17:59:26 +0100
commita0fc92564e6db5dafce53c7eba11f413a2121819 (patch)
treeb0030faffdf99a1d157a2efb083f75939e902e1e /src/file_tiff.h
parent7f8425d8398ea96a9d5e9a99f3c4ed58c2485215 (diff)
src/file_jpg.c: make code more frama-c friendly, file_tiff* modified to
help
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h26
1 files changed, 17 insertions, 9 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index 3cd6a63..b030da2 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -71,24 +71,30 @@ struct ifd_header {
/*@
@ requires buffer_size >= sizeof(TIFFHeader);
@ requires \valid_read(buffer+(0..buffer_size-1));
+ @ ensures \valid_read(buffer+(0..buffer_size-1));
@*/
time_t get_date_from_tiff_header(const unsigned char*buffer, const unsigned int buffer_size);
/*@
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \separated(potential_error, buffer);
+ @ ensures \valid_read(buffer+(0..buffer_size-1));
@*/
-unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int tag, const char **potential_error);
+unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int tag, const unsigned char **potential_error);
-#ifndef MAIN_tiff_be
+#if !defined(MAIN_tiff_be)
/*@
@ requires tiff_size >= sizeof(TIFFHeader);
- @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires tiff_size >= sizeof(struct ifd_header);
+ @ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
- @ requires \separated(potential_error, tiff);
+ @ requires \separated(potential_error, buffer);
+ @ ensures \valid_read(buffer+(0..tiff_size-1));
@*/
-const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
+unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
+#endif
+#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg)
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
@@ -113,14 +119,16 @@ void file_check_tiff_le(file_recovery_t *fr);
int header_check_tiff_le(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);
#endif
-#ifndef MAIN_tiff_le
+#if !defined(MAIN_tiff_le)
/*@
@ requires tiff_size >= sizeof(TIFFHeader);
- @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires tiff_size >= sizeof(struct ifd_header);
+ @ requires \valid_read(buffer+(0..tiff_size-1));
@ requires \valid(potential_error);
- @ requires \separated(potential_error, tiff);
+ @ requires \separated(potential_error, buffer);
+ @ ensures \valid_read(buffer+(0..tiff_size-1));
@*/
-const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
+unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error);
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)