summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:18:17 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-18 10:18:17 +0100
commit9b51c2aeb03fe414b7946043ad39e7ab0b1d0cf9 (patch)
tree3f301f91ee168a27f3024b274dd98f53b9af8f67 /src/file_tiff.h
parent611da961b33b7d1d0b68a8d7f87437417055dab5 (diff)
PhotoRec - file_tiff*.c: Reintroduce fixed IFD1 parsing.
Buggy version was removed by commit 7e8f99aa92038220efa4d9c45cf8a0857a77d7d8
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h24
1 files changed, 21 insertions, 3 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index 51059f5..fa9af03 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -77,7 +77,7 @@ time_t get_date_from_tiff_header(const unsigned char*buffer, const unsigned int
/*@
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \separated(potential_error, buffer);
- @ ensures \valid_read(buffer+(0..buffer_size-1));
+ @ assigns *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);
@@ -88,7 +88,7 @@ unsigned int find_tag_from_tiff_header(const unsigned char *buffer, const unsign
@ 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));
+ @ assigns *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
@@ -109,12 +109,21 @@ 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 file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_tiff_le);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, 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
@@ -126,7 +135,7 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
@ 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));
+ @ assigns *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
@@ -136,11 +145,20 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char*buffer, const unsi
@ requires buffer_size >= 15;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid_read(file_recovery);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures \result == 1 ==> \initialized(&file_recovery_new->time);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename== \null);
@ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
@ ensures (\result == 1) ==> valid_read_string(file_recovery_new->extension);
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, 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