summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-24 19:04:06 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-24 19:04:06 +0200
commit990e81e4d9269fdac3c4768878256b576ca3d203 (patch)
tree9f9c490f861de03e4d244b863bbedda18a5aa445 /src/file_tiff.h
parent2b90bb8947809de472ecc37fa79f895af2f0435b (diff)
file_tiff: make the code more frama-c friendly
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h64
1 files changed, 34 insertions, 30 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index 5ef2325..aaac994 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -22,6 +22,7 @@
#ifdef __cplusplus
extern "C" {
#endif
+
#define TIFF_ERROR 0xffffffffffffffffull
#define TIFF_BIGENDIAN 0x4d4d
@@ -78,18 +79,7 @@ time_t get_date_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff
@*/
const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char **potential_error);
-/*@
- @ requires \valid(file_recovery);
- @ requires \valid(file_recovery->handle);
- @*/
-void file_check_tiff(file_recovery_t *file_recovery);
-
-/*@
- @ requires tiff_size >= sizeof(TIFFHeader);
- @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
- @ requires \valid(potential_error);
- @*/
-const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
+#ifndef MAIN_tiff_be
/*@
@ requires tiff_size >= sizeof(TIFFHeader);
@ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
@@ -101,31 +91,45 @@ const char *find_tag_from_tiff_header_le(const TIFFHeader *tiff, const unsigned
@ requires \valid(fr);
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
- @ requires \initialized(&fr->extension);
- @
- */
-uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
+ @ requires valid_read_string(fr->extension);
+ @*/
+void file_check_tiff_le(file_recovery_t *fr);
/*@
- @ requires \valid(fr);
- @ requires \valid(fr->handle);
- @ requires \valid_read(&fr->extension);
- @ requires \initialized(&fr->extension);
- @
- */
-uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count);
+ @ 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
+#ifndef MAIN_tiff_le
/*@
- @ requires \valid_read(buffer+(0..buffer_size-1));
- @
- */
-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);
+ @ requires tiff_size >= sizeof(TIFFHeader);
+ @ requires \valid_read((const unsigned char *)tiff+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @*/
+const char *find_tag_from_tiff_header_be(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error);
/*@
+ @ requires buffer_size >= 15;
@ requires \valid_read(buffer+(0..buffer_size-1));
- @
- */
-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);
+ @ 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_be);
+ @ 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
unsigned int tiff_type2size(const unsigned int type);
#ifdef DEBUG_TIFF