summaryrefslogtreecommitdiffstats
path: root/src/file_tiff_le.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_tiff_le.c')
-rw-r--r--src/file_tiff_le.c565
1 files changed, 439 insertions, 126 deletions
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 2a4aa92..590e7bf 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -38,106 +38,173 @@
#include "common.h"
#include "file_tiff.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
extern const file_hint_t file_hint_raf;
+#endif
+#if (!defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)) || defined(MAIN_jpg)
extern const file_hint_t file_hint_jpg;
+#endif
+extern const file_hint_t file_hint_tiff;
+static const char *extension_arw="arw";
+static const char *extension_cr2="cr2";
+static const char *extension_dng="dng";
+static const char *extension_nef="nef";
+static const char *extension_sr2="sr2";
-static const char *find_tag_from_tiff_header_le_aux(const TIFFHeader *tiff, const unsigned int tiff_size, const unsigned int tag, const char**potential_error, const struct ifd_header *hdr)
+#ifndef MAIN_tiff_be
+/*@
+ @ requires \valid_read(buffer+(0..tiff_size-1));
+ @ requires \valid(potential_error);
+ @ requires \separated(potential_error, buffer+(..));
+ @
+ */
+static unsigned int find_tag_from_tiff_header_le_aux(const unsigned char *buffer, const unsigned int tiff_size, const unsigned int tag, const unsigned char**potential_error, const unsigned int offset_hdr)
{
- const TIFFDirEntry *tmp;
+ const unsigned char *ptr_hdr;
+ const struct ifd_header *hdr;
unsigned int i;
unsigned int nbr_fields;
- /* Bound checking */
- if((const char*)(hdr) <= (const char*)tiff ||
- (const char*)(hdr+1) > (const char*)tiff+tiff_size)
- return NULL;
+ if(sizeof(struct ifd_header) > tiff_size)
+ return 0;
+ /*@ assert tiff_size >= sizeof(struct ifd_header); */
+ if(offset_hdr > tiff_size - sizeof(struct ifd_header))
+ return 0;
+ /*@ assert offset_hdr + sizeof(struct ifd_header) <= tiff_size; */
+ ptr_hdr=&buffer[offset_hdr];
+ /*@ assert \valid_read(ptr_hdr + (0 .. sizeof(struct ifd_header)-1)); */
+ hdr=(const struct ifd_header *)ptr_hdr;
+ /*@ assert \valid_read(hdr); */
nbr_fields=le16(hdr->nbr_fields);
- for(i=0, tmp=&hdr->ifd;
- i < nbr_fields && (const char*)(tmp+1) <= (const char*)tiff+tiff_size;
- i++, tmp++)
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ /*@
+ @ loop assigns i, *potential_error;
+ @ loop variant nbr_fields - i;
+ @*/
+ for(i=0; i < nbr_fields; i++)
{
- if(le16(tmp->tdir_type) > 18 && (*potential_error==NULL || *potential_error > (const char*)&tmp->tdir_type+1))
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ const unsigned int offset_entry=offset_hdr + 2 + i * sizeof(TIFFDirEntry);
+ const unsigned char *ptr_entry;
+ const TIFFDirEntry *tmp;
+ if(offset_entry + sizeof(TIFFDirEntry) > tiff_size)
+ return 0;
+ /*@ assert offset_entry + sizeof(TIFFDirEntry) <= tiff_size; */
+ /*X assert \valid_read(buffer + (0 .. offset_entry + sizeof(TIFFDirEntry)-1)); */
+ /*X assert \valid_read((buffer + offset_entry) + (0 .. sizeof(TIFFDirEntry)-1)); */
+ ptr_entry=buffer + offset_entry;
+ /*@ assert \valid_read(ptr_entry + (0 .. sizeof(TIFFDirEntry)-1)); */
+ tmp=(const TIFFDirEntry *)ptr_entry;
+ /*@ assert \valid_read(tmp); */
+ if(le16(tmp->tdir_type) > 18 && (*potential_error==NULL || *potential_error > (const unsigned char*)&tmp->tdir_type))
{
- *potential_error = (const char*)&tmp->tdir_type+1;
+ *potential_error = (const unsigned char*)&tmp->tdir_type;
}
if(le16(tmp->tdir_tag)==tag)
- return (const char*)tiff+le32(tmp->tdir_offset);
+ {
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ return le32(tmp->tdir_offset);
+ }
}
- return NULL;
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ return 0;
}
-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)
{
- const struct ifd_header *ifd0;
- const struct ifd_header *exififd;
- const uint32_t *tiff_next_diroff;
- if(tiff_size < sizeof(TIFFHeader))
- return NULL;
- if(tiff_size < le32(tiff->tiff_diroff)+sizeof(TIFFDirEntry))
- return NULL;
- ifd0=(const struct ifd_header *)((const char*)tiff + le32(tiff->tiff_diroff));
- /* Bound checking */
- if((const char*)ifd0 < (const char*)tiff ||
- (const char*)(ifd0+1) > (const char*)tiff + tiff_size)
- return NULL;
+ /*@ assert tiff_size >= sizeof(TIFFHeader); */
+ /*@ assert tiff_size >= sizeof(struct ifd_header); */
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ const TIFFHeader *tiff=(const TIFFHeader *)buffer;
+ unsigned int offset_ifd0;
+ unsigned int offset_exififd;
+ /*@ assert \valid_read(tiff); */
+ offset_ifd0=le32(tiff->tiff_diroff);
+ if(offset_ifd0 >= tiff_size)
+ return 0;
+ /*@ assert offset_ifd0 < tiff_size; */
+ if(offset_ifd0 > tiff_size - sizeof(struct ifd_header))
+ return 0;
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ /*@ assert offset_ifd0 + sizeof(struct ifd_header) <= tiff_size; */
{
- const char *tmp=find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, ifd0);
+ const unsigned int tmp=find_tag_from_tiff_header_le_aux(buffer, tiff_size, tag, potential_error, offset_ifd0);
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
if(tmp)
return tmp;
}
- exififd=(const struct ifd_header *)find_tag_from_tiff_header_le_aux(tiff, tiff_size, TIFFTAG_EXIFIFD, potential_error, ifd0);
- if(exififd!=NULL)
+ offset_exififd=find_tag_from_tiff_header_le_aux(buffer, tiff_size, TIFFTAG_EXIFIFD, potential_error, offset_ifd0);
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ if(offset_exififd <= tiff_size - sizeof(struct ifd_header))
{
/* Exif */
- const char *tmp=find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, exififd);
+ const unsigned int tmp=find_tag_from_tiff_header_le_aux(buffer, tiff_size, tag, potential_error, offset_exififd);
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
if(tmp)
return tmp;
}
- tiff_next_diroff=(const uint32_t *)(&ifd0->ifd + le16(ifd0->nbr_fields));
- if( (const char *)tiff_next_diroff >= (const char *)tiff &&
- (const char *)(tiff_next_diroff + 1) < (const char*)tiff + tiff_size &&
- le32(*tiff_next_diroff)>0)
- {
- /* IFD1 */
- const struct ifd_header *ifd1=(const struct ifd_header*)((const char *)tiff+le32(*tiff_next_diroff));
- return find_tag_from_tiff_header_le_aux(tiff, tiff_size, tag, potential_error, ifd1);
- }
- return NULL;
+ /*@ assert \valid_read(buffer+(0..tiff_size-1)); */
+ return 0;
}
+#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg)
+/*@
+ @ requires \valid(handle);
+ @ requires \valid_read(entry_strip_offsets);
+ @ requires \valid_read(entry_strip_bytecounts);
+ @*/
static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_offsets, const TIFFDirEntry *entry_strip_bytecounts)
{
const unsigned int nbr=(le32(entry_strip_offsets->tdir_count)<2048?
le32(entry_strip_offsets->tdir_count):
2048);
+ /*@ assert nbr <= 2048; */
unsigned int i;
uint32_t *offsetp;
uint32_t *sizep;
uint64_t max_offset=0;
- if(le32(entry_strip_offsets->tdir_count) != le32(entry_strip_bytecounts->tdir_count))
- return -1;
- if(le32(entry_strip_offsets->tdir_count)==0 ||
+ /* le32() isn't required to compare the 2 values */
+ if(entry_strip_offsets->tdir_count != entry_strip_bytecounts->tdir_count)
+ return TIFF_ERROR;
+ /*@ assert entry_strip_offsets->tdir_count == entry_strip_bytecounts->tdir_count; */
+ if(nbr==0 ||
le16(entry_strip_offsets->tdir_type)!=4 ||
le16(entry_strip_bytecounts->tdir_type)!=4)
- return -1;
+ return TIFF_ERROR;
+ /*@ assert 0 < nbr <= 2048; */
+#ifdef __FRAMAC__
+ offsetp=(uint32_t *)MALLOC(2048*sizeof(*offsetp));
+#else
offsetp=(uint32_t *)MALLOC(nbr*sizeof(*offsetp));
+#endif
if(fseek(handle, le32(entry_strip_offsets->tdir_offset), SEEK_SET) < 0 ||
fread(offsetp, sizeof(*offsetp), nbr, handle) != nbr)
{
free(offsetp);
- return -1;
+ return TIFF_ERROR;
}
+#ifdef __FRAMAC__
+ sizep=(uint32_t *)MALLOC(2048*sizeof(*sizep));
+#else
sizep=(uint32_t *)MALLOC(nbr*sizeof(*sizep));
+#endif
if(fseek(handle, le32(entry_strip_bytecounts->tdir_offset), SEEK_SET) < 0 ||
fread(sizep, sizeof(*sizep), nbr, handle) != nbr)
{
free(offsetp);
free(sizep);
- return -1;
+ return TIFF_ERROR;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)offsetp, nbr*sizeof(*offsetp));
+ Frama_C_make_unknown((char *)sizep, nbr*sizeof(*sizep));
+#endif
for(i=0; i<nbr; i++)
{
- const uint64_t tmp=le32(offsetp[i]) + le32(sizep[i]);
+ const uint64_t tmp=(uint64_t)le32(offsetp[i]) + le32(sizep[i]);
if(max_offset < tmp)
max_offset=tmp;
}
@@ -146,6 +213,11 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
return max_offset;
}
+/*@
+ @ requires type != 1 || \valid_read((const char *)val);
+ @ requires type != 3 || \valid_read((const char *)val + ( 0 .. 2));
+ @ requires type != 4 || \valid_read((const char *)val + ( 0 .. 4));
+ @*/
static unsigned int tiff_le_read(const void *val, const unsigned int type)
{
switch(type)
@@ -160,6 +232,7 @@ static unsigned int tiff_le_read(const void *val, const unsigned int type)
return 0;
}
}
+#endif
#ifdef ENABLE_TIFF_MAKERNOTE
static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
@@ -183,12 +256,17 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
uint64_t tile_bytecounts=0;
const TIFFDirEntry *entry;
if(tiff_diroff < sizeof(TIFFHeader))
- return -1;
+ return TIFF_ERROR;
if(fseek(in, tiff_diroff, SEEK_SET) < 0)
- return -1;
+ return TIFF_ERROR;
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
- return -1;
+ return TIFF_ERROR;
+ /*@ assert data_read >= 2; */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, sizeof(buffer));
+#endif
+ /*@ assert 2 <= data_read <= sizeof(buffer); */
if( memcmp(buffer, sign_nikon1, sizeof(sign_nikon1))==0 ||
memcmp(buffer, sign_nikon2, sizeof(sign_nikon2))==0 ||
memcmp(buffer, sign_pentax, sizeof(sign_pentax))==0 )
@@ -199,10 +277,10 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
log_info("tiff_le_makernote(%lu) => %u entries\n", (long unsigned)tiff_diroff, n);
#endif
//sizeof(TIFFDirEntry)=12;
- if(n > (unsigned)(data_read-2)/12)
+ if(n > (unsigned int)(data_read-2)/12)
n=(data_read-2)/12;
if(n==0)
- return -1;
+ return TIFF_ERROR;
for(i=0;i<n;i++)
{
const uint64_t val=(uint64_t)le32(entry->tdir_count) * tiff_type2size(le16(entry->tdir_type));
@@ -221,7 +299,7 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
{
const uint64_t new_offset=le32(entry->tdir_offset)+val;
if(new_offset==0)
- return -1;
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -259,13 +337,63 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
return max_offset;
}
#endif
+#endif
+
+#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg)
+static uint64_t file_check_tiff_le_aux(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)
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires valid_read_string(fr->extension);
+ @ requires \separated(&errno, fr);
+ @ requires \valid_read(buffer + (0 .. buffer_size - 1));
+ @ ensures \valid(fr);
+ @ ensures \valid(fr->handle);
+ @ ensures valid_read_string(fr->extension);
+ @*/
+static uint64_t file_check_tiff_le_aux_next(file_recovery_t *fr, const unsigned int depth, const unsigned int count, const unsigned char *buffer, const unsigned int buffer_size, const unsigned int offset_ptr_offset)
+{
+ if(buffer_size < 4)
+ return 0;
+ /*@ assert buffer_size >= 4; */
+ if(offset_ptr_offset > buffer_size-4)
+ return 0;
+ {
+ /*@ assert offset_ptr_offset <= buffer_size - 4; */
+ /*@ assert offset_ptr_offset + 4 <= buffer_size; */
+ /*@ assert \valid_read(buffer + (0 .. offset_ptr_offset + 4 - 1)); */
+ const unsigned char *ptr_offset=&buffer[offset_ptr_offset];
+ /*@ assert \valid_read(ptr_offset + (0 .. 4 - 1)); */
+ const uint32_t *ptr32_offset=(const uint32_t *)ptr_offset;
+ /*@ assert \valid_read(ptr32_offset); */
+ const unsigned int next_diroff=le32(*ptr32_offset);
+ if(next_diroff == 0)
+ return 0;
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ return file_check_tiff_le_aux(fr, next_diroff, depth+1, count+1);
+ }
+}
+
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires valid_read_string(fr->extension);
+ @ requires \separated(&errno, fr);
+ @ ensures \valid(fr);
+ @ ensures \valid(fr->handle);
+ @ ensures valid_read_string(fr->extension);
+ @*/
+static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
unsigned int i,n;
int data_read;
- const uint32_t *tiff_next_diroff;
uint64_t max_offset=0;
uint64_t alphaoffset=0;
uint64_t alphabytecount=0;
@@ -279,38 +407,58 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
uint64_t tile_bytecounts=0;
unsigned int tdir_tag_old=0;
unsigned int sorted_tag_error=0;
- const TIFFDirEntry *entry=(const TIFFDirEntry *)&buffer[2];
+ const TIFFDirEntry *entries=(const TIFFDirEntry *)&buffer[2];
const TIFFDirEntry *entry_strip_offsets=NULL;
const TIFFDirEntry *entry_strip_bytecounts=NULL;
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_le(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
+ log_info("file_check_tiff_le_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
if(depth>4)
- return -1;
+ return TIFF_ERROR;
if(count>16)
- return -1;
+ return TIFF_ERROR;
if(tiff_diroff < sizeof(TIFFHeader))
- return -1;
+ return TIFF_ERROR;
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
- return -1;
+ return TIFF_ERROR;
data_read=fread(buffer, 1, sizeof(buffer), fr->handle);
+#if defined(__FRAMAC__)
+ data_read = Frama_C_interval(0, sizeof(buffer));
+ /*@ assert 0 <= data_read <= sizeof(buffer); */
+ Frama_C_make_unknown((char *)buffer, sizeof(buffer));
+#endif
if(data_read<2)
- return -1;
- n=buffer[0]+(buffer[1]<<8);
+ return TIFF_ERROR;
+ /*@ assert 2 <= data_read <= sizeof(buffer); */
+ n=buffer[0] | (buffer[1]<<8);
#ifdef DEBUG_TIFF
- log_info("header_check_tiff_le(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
+ log_info("file_check_tiff_le_aux(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
#endif
- //sizeof(TIFFDirEntry)=12;
- if(n > (unsigned)(data_read-2)/12)
- n=(data_read-2)/12;
if(n==0)
- return -1;
- for(i=0;i<n;i++)
+ return TIFF_ERROR;
+ /*@ assert 0 < n <= 65535; */
+ /*@ assert sizeof(TIFFDirEntry)==12; */
+ /*X
+ X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
+ X loop variant n-i;
+ X*/
+ for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
{
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ const TIFFDirEntry *entry=&entries[i];
+ /*@ assert 0 <= i < n; */
+ /*@ assert \valid_read(entry); */
+ const unsigned int tdir_count=le32(entry->tdir_count);
const unsigned int tdir_tag=le16(entry->tdir_tag);
- const uint64_t val=(uint64_t)le32(entry->tdir_count) * tiff_type2size(le16(entry->tdir_type));
+ const uint64_t val=(uint64_t)tdir_count * tiff_type2size(le16(entry->tdir_type));
#ifdef DEBUG_TIFF
log_info("%u tag=%u(0x%x) %s type=%u count=%lu offset=%lu(0x%lx) val=%lu\n",
i,
@@ -318,26 +466,30 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
tdir_tag,
tag_name(tdir_tag),
le16(entry->tdir_type),
- (long unsigned)le32(entry->tdir_count),
+ (long unsigned)tdir_count,
(long unsigned)le32(entry->tdir_offset),
(long unsigned)le32(entry->tdir_offset),
(long unsigned)val);
#endif
if(tdir_tag_old > tdir_tag)
- { /* Entries must be sorted by tag, some SR2 file doesn't respected this rule */
- sorted_tag_error++;
- if(sorted_tag_error > 1 && strcmp(fr->extension,"sr2")!=0)
- return -1;
+ { /* Entries must be sorted by tag, some SR2 files don't respect this rule */
+ if(sorted_tag_error > 0)
+ {
+ if(fr->extension != extension_sr2)
+ return TIFF_ERROR;
+ }
+ else
+ sorted_tag_error=1;
}
if(val>4)
{
const uint64_t new_offset=le32(entry->tdir_offset)+val;
if(new_offset==0)
- return -1;
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
- if(le32(entry->tdir_count)==1 && val<=4)
+ if(tdir_count==1 && val<=4)
{
const unsigned int tmp=tiff_le_read(&entry->tdir_offset, le16(entry->tdir_type));
switch(tdir_tag)
@@ -355,15 +507,23 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
{
- const uint64_t new_offset=header_check_tiff_le(fr, tmp, depth+1, 0);
- if(new_offset==-1)
- return -1;
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ if(new_offset==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
break;
case TIFFTAG_SUBIFD:
- if(fr->extension!=NULL && strcmp(fr->extension, "arw")==0)
+ if(fr->extension == extension_arw)
{
/* DSLR-A100 is boggus, may be A100DataOffset */
if(max_offset < tmp)
@@ -371,9 +531,17 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
else
{
- const uint64_t new_offset=header_check_tiff_le(fr, tmp, depth+1, 0);
- if(new_offset==-1)
- return -1;
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ if(new_offset==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -382,8 +550,8 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
case EXIFTAG_MAKERNOTE:
{
const uint64_t new_offset=tiff_le_makernote(fr->handle, tmp);
- if(new_offset==-1)
- return -1;
+ if(new_offset==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
@@ -391,8 +559,9 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
#endif
}
}
- else if(le32(entry->tdir_count) > 1)
+ else if(tdir_count > 1)
{
+ /*@ assert tdir_count > 1; */
switch(tdir_tag)
{
case TIFFTAG_EXIFIFD:
@@ -400,31 +569,43 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
case TIFFTAG_SUBIFD:
if(le16(entry->tdir_type)==4)
{
- const unsigned int nbr=(le32(entry->tdir_count)<32?le32(entry->tdir_count):32);
+ const unsigned int nbr=(tdir_count<32?tdir_count:32);
+ /*@ assert 2 <= nbr <= 32; */
+ uint32_t subifd_offsetp[32];
unsigned int j;
- uint32_t *subifd_offsetp;
if(fseek(fr->handle, le32(entry->tdir_offset), SEEK_SET) < 0)
{
- return -1;
+ return TIFF_ERROR;
}
- subifd_offsetp=(uint32_t *)MALLOC(nbr*sizeof(*subifd_offsetp));
- if(fread(subifd_offsetp, sizeof(*subifd_offsetp), nbr, fr->handle) != nbr)
+ if(fread(subifd_offsetp, sizeof(uint32_t), nbr, fr->handle) != nbr)
{
- free(subifd_offsetp);
- return -1;
+ return TIFF_ERROR;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
+#endif
+ /*X
+ X loop invariant 0 <= j <= nbr <=32;
+ X loop variant nbr-j;
+ X*/
for(j=0; j<nbr; j++)
{
- const uint64_t new_offset=header_check_tiff_le(fr, le32(subifd_offsetp[j]), depth+1, 0);
- if(new_offset==-1)
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(subifd_offsetp[j]), depth+1, 0);
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ if(new_offset==TIFF_ERROR)
{
- free(subifd_offsetp);
- return -1;
+ return TIFF_ERROR;
}
if(max_offset < new_offset)
max_offset = new_offset;
}
- free(subifd_offsetp);
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -442,7 +623,6 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
}
}
tdir_tag_old=tdir_tag;
- entry++;
}
if(alphabytecount > 0 && max_offset < alphaoffset + alphabytecount)
max_offset = alphaoffset + alphabytecount;
@@ -459,78 +639,211 @@ uint64_t header_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, c
if(entry_strip_offsets != NULL && entry_strip_bytecounts != NULL)
{
const uint64_t tmp=parse_strip_le(fr->handle, entry_strip_offsets, entry_strip_bytecounts);
- if(tmp==-1)
- return -1;
+ if(tmp==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < tmp)
max_offset=tmp;
}
if(entry_tile_offsets != NULL && entry_tile_bytecounts != NULL)
{
const uint64_t tmp=parse_strip_le(fr->handle, entry_tile_offsets, entry_tile_bytecounts);
- if(tmp==-1)
- return -1;
+ if(tmp==TIFF_ERROR)
+ return TIFF_ERROR;
if(max_offset < tmp)
max_offset=tmp;
}
- tiff_next_diroff=(const uint32_t *)entry;
- if(le32(*tiff_next_diroff) > 0)
{
- const uint64_t new_offset=header_check_tiff_le(fr, le32(*tiff_next_diroff), depth+1, count+1);
- if(new_offset != -1 && max_offset < new_offset)
+ const unsigned int offset_ptr_offset=2+12*n;
+ const uint64_t new_offset=file_check_tiff_le_aux_next(fr, depth, count, buffer, data_read, offset_ptr_offset);
+ /*@ assert \valid(fr); */
+ /*@ assert \valid(fr->handle); */
+ /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_read_string(fr->extension); */
+ if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
return max_offset;
}
-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)
+void file_check_tiff_le(file_recovery_t *fr)
{
- const char raf_fp[15]={0x49, 0x49, 0x2a, 0x00, 0x08, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0xf0, 0x0d, 0x00, 0x01};
- const char *potential_error=NULL;
+ static uint64_t calculated_file_size=0;
+ TIFFHeader header;
+ calculated_file_size = 0;
+ if(fseek(fr->handle, 0, SEEK_SET) < 0 ||
+ fread(&header, sizeof(TIFFHeader), 1, fr->handle) != 1)
+ {
+ fr->file_size=0;
+ return;
+ }
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&header, sizeof(TIFFHeader));
+#endif
+ if(header.tiff_magic==TIFF_LITTLEENDIAN)
+ calculated_file_size=file_check_tiff_le_aux(fr, le32(header.tiff_diroff), 0, 0);
+ /*@ assert \valid(fr->handle); */
+#ifdef DEBUG_TIFF
+ log_info("TIFF Current %llu\n", (unsigned long long)fr->file_size);
+ log_info("TIFF Estimated %llu %llx\n", (unsigned long long)calculated_file_size, (unsigned long long)calculated_file_size);
+#endif
+ if(fr->file_size < calculated_file_size || calculated_file_size==0 || calculated_file_size==TIFF_ERROR)
+ fr->file_size=0;
+ /* PhotoRec isn't yet capable to find the correct filesize for
+ * Sony arw and dng,
+ * Panasonic raw/rw2,
+ * Minolta tif
+ * Sony sr2
+ * so don't truncate them */
+ else if(strcmp(fr->extension,"cr2")==0 ||
+ strcmp(fr->extension,"dcr")==0 ||
+ strcmp(fr->extension,"nef")==0 ||
+ strcmp(fr->extension,"orf")==0 ||
+ strcmp(fr->extension,"pef")==0 ||
+ (strcmp(fr->extension,"tif")==0 && calculated_file_size>1024*1024*1024) ||
+ strcmp(fr->extension,"wdp")==0)
+ fr->file_size=calculated_file_size;
+}
+#endif
+
+#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg)
+/*@
+ @ requires separation: \separated(&file_hint_tiff, buffer+(..), file_recovery, file_recovery_new);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_tiff.extension ||
+ file_recovery_new->extension == extension_arw ||
+ file_recovery_new->extension == extension_cr2 ||
+ file_recovery_new->extension == extension_dng ||
+ file_recovery_new->extension == extension_nef ||
+ file_recovery_new->extension == extension_sr2);
+ @*/
+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)
+{
+ const unsigned char raf_fp[15]={0x49, 0x49, 0x2a, 0x00, 0x08, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0xf0, 0x0d, 0x00, 0x01};
+ const unsigned char *potential_error=NULL;
const TIFFHeader *header=(const TIFFHeader *)buffer;
if((uint32_t)le32(header->tiff_diroff) < sizeof(TIFFHeader))
return 0;
/* Avoid a false positiv with some RAF files */
if(file_recovery->file_stat!=NULL &&
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
file_recovery->file_stat->file_hint==&file_hint_raf &&
+#endif
memcmp(buffer, raf_fp, 15)==0)
{
header_ignored(file_recovery_new);
return 0;
}
+#if (!defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)) || defined(MAIN_jpg)
if(file_recovery->file_stat!=NULL &&
file_recovery->file_stat->file_hint==&file_hint_jpg)
{
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
+#endif
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="tif";
+ file_recovery_new->extension=file_hint_tiff.extension;
/* Canon RAW */
if(buffer[8]=='C' && buffer[9]=='R' && buffer[10]==2)
- file_recovery_new->extension="cr2";
- else if(find_tag_from_tiff_header_le(header, buffer_size, TIFFTAG_DNGVERSION, &potential_error)!=NULL)
+ file_recovery_new->extension=extension_cr2;
+ else if(find_tag_from_tiff_header_le(buffer, buffer_size, TIFFTAG_DNGVERSION, &potential_error)!=0)
{
/* Adobe Digital Negative, ie. NIKON D50 */
- file_recovery_new->extension="dng";
+ file_recovery_new->extension=extension_dng;
}
else
{
- const char *tag_make;
- tag_make=find_tag_from_tiff_header_le(header, buffer_size, TIFFTAG_MAKE, &potential_error);
- if(tag_make!=NULL && tag_make >= (const char *)buffer && tag_make < (const char *)buffer + buffer_size - 5)
+ const unsigned int tag_make=find_tag_from_tiff_header_le(buffer, buffer_size, TIFFTAG_MAKE, &potential_error);
+ if(tag_make!=0 && tag_make < buffer_size - 5)
{
/* TODO
* sr2 if Sony::FileFormat begins by 1
* arw otherwise */
- if(memcmp(tag_make, "SONY", 5)==0)
- file_recovery_new->extension="sr2";
- else if(strncmp(tag_make, "SONY ",5)==0)
- file_recovery_new->extension="arw";
- else if(memcmp(tag_make, "NIKON CORPORATION", 18)==0)
- file_recovery_new->extension="nef";
+ if(memcmp(&buffer[tag_make], "SONY", 5)==0)
+ file_recovery_new->extension=extension_sr2;
+ else if(memcmp(&buffer[tag_make], "SONY ",5)==0)
+ file_recovery_new->extension=extension_arw;
+ else if(tag_make < buffer_size - 18 && memcmp(&buffer[tag_make], "NIKON CORPORATION", 18)==0)
+ file_recovery_new->extension=extension_nef;
}
}
- file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
- file_recovery_new->file_check=&file_check_tiff;
+ file_recovery_new->time=get_date_from_tiff_header(buffer, buffer_size);
+ file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
+#endif
+
+#if defined(MAIN_tiff_le)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.tif";
+ unsigned char buffer[BLOCKSIZE];
+ int res;
+ file_recovery_t file_recovery_new;
+ file_recovery_t file_recovery;
+ file_stat_t file_stats;
+
+ /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+
+ reset_file_recovery(&file_recovery);
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_recovery_new.data_check=NULL;
+ file_recovery_new.extension=NULL;
+ file_recovery_new.file_stat=NULL;
+ file_recovery_new.file_check=NULL;
+ file_recovery_new.file_rename=NULL;
+ file_recovery_new.calculated_file_size=0;
+ file_recovery_new.file_size=0;
+ file_recovery_new.location.start=0;
+
+ file_stats.file_hint=&file_hint_tiff;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ file_hint_tiff.register_header_check(&file_stats);
+ if(header_check_tiff_le(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert file_recovery_new.file_check == &file_check_tiff_le; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert file_recovery_new.extension == file_hint_tiff.extension ||
+ file_recovery_new.extension == extension_arw ||
+ file_recovery_new.extension == extension_cr2 ||
+ file_recovery_new.extension == extension_dng ||
+ file_recovery_new.extension == extension_nef ||
+ file_recovery_new.extension == extension_sr2; */
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.data_check == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
+ {
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ header_check_tiff_le(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.file_check == &file_check_tiff_le; */
+ {
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_tiff_le(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ return 0;
+}
+#endif