summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h87
1 files changed, 78 insertions, 9 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index ed2f86c..51059f5 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -23,6 +23,8 @@
extern "C" {
#endif
+#define TIFF_ERROR 0xffffffffffffffffull
+
#define TIFF_BIGENDIAN 0x4d4d
#define TIFF_LITTLEENDIAN 0x4949
#define TIFFTAG_IMAGEDESCRIPTION 270 /* info about image */
@@ -66,16 +68,83 @@ struct ifd_header {
TIFFDirEntry ifd;
} __attribute__ ((gcc_struct, __packed__));
-time_t get_date_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size);
-const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char **potential_error);
-void file_check_tiff(file_recovery_t *file_recovery);
+/*@
+ @ 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 unsigned char **potential_error);
+
+#if !defined(MAIN_tiff_be)
+/*@
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires tiff_size >= sizeof(struct ifd_header);
+ @ requires \valid_read(buffer+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @ requires \separated(potential_error, buffer);
+ @ ensures \valid_read(buffer+(0..tiff_size-1));
+ @*/
+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);
+ @ requires \valid_read(&fr->extension);
+ @ requires valid_read_string(fr->extension);
+ @ requires fr->file_check==&file_check_tiff_le;
+ @ ensures \valid(fr->handle);
+ @ ensures valid_read_string(fr->extension);
+ @*/
+void file_check_tiff_le(file_recovery_t *fr);
+
+/*@
+ @ requires buffer_size >= 15;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
+ @ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @*/
+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
+
+#if !defined(MAIN_tiff_le)
+/*@
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires tiff_size >= sizeof(struct ifd_header);
+ @ requires \valid_read(buffer+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @ requires \separated(potential_error, buffer);
+ @ ensures \valid_read(buffer+(0..tiff_size-1));
+ @*/
+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)
+/*@
+ @ requires buffer_size >= 15;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
+ @ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @*/
+int header_check_tiff_be(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
-const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
-const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
-uint64_t header_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
-uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
-int header_check_tiff_be_new(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);
-int header_check_tiff_le_new(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);
unsigned int tiff_type2size(const unsigned int type);
#ifdef DEBUG_TIFF
const char *tag_name(unsigned int tag);