summaryrefslogtreecommitdiffstats
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
parent2b90bb8947809de472ecc37fa79f895af2f0435b (diff)
file_tiff: make the code more frama-c friendly
-rw-r--r--Makefile.am7
-rw-r--r--src/file_orf.c2
-rw-r--r--src/file_rw2.c2
-rw-r--r--src/file_tiff.c48
-rw-r--r--src/file_tiff.h64
-rw-r--r--src/file_tiff_be.c137
-rw-r--r--src/file_tiff_le.c218
-rw-r--r--src/file_wdp.c2
-rw-r--r--src/filegen.h1
9 files changed, 366 insertions, 115 deletions
diff --git a/Makefile.am b/Makefile.am
index 445872e..7f41dd2 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -80,6 +80,10 @@ extras:
extrasstatic:
$(MAKE) LDFLAGS="$(LDFLAGS) -static" LIBS="$(PTHREAD_LIBS) $(LIBS)" CFLAGS="$(PTHREAD_CFLAGS) $(CFLAGS)" CXXFLAGS="$(PTHREAD_CFLAGS) $(CXXFLAGS)" extras
+session_tiff_be.framac: src/file_tiff.c src/file_tiff_be.c src/file_tiff_le.c src/common.c src/filegen.c src/log.c
+ gcc -W -Wall -DMAIN_tiff_le -DHAVE_CONFIG_H -O -o demo -I. $^
+ frama-c $^ -cpp-extra-args="-DMAIN_tiff_le -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
+
session_tiff_le.framac: src/file_tiff.c src/file_tiff_be.c src/file_tiff_le.c src/common.c src/filegen.c src/log.c
gcc -W -Wall -DMAIN_tiff_le -DHAVE_CONFIG_H -O -o demo -I. $^
frama-c $^ -cpp-extra-args="-DMAIN_tiff_le -DHAVE_CONFIG_H -D__x86_64__" $(FRAMA_C_FLAGS) -save $@
@@ -99,4 +103,7 @@ session_%.framac: src/file_%.c src/common.c src/filegen.c src/log.c
frama-c-%: session_%.framac
frama-c-gui -load $^
+cppcheck:
+ cppcheck --quiet --enable=all -DHAVE_CONFIG_H -I$(builddir) -I/usr/include $(srcdir)/src
+
DISTCLEANFILES = *~ core
diff --git a/src/file_orf.c b/src/file_orf.c
index bf3f5b1..71895e8 100644
--- a/src/file_orf.c
+++ b/src/file_orf.c
@@ -54,7 +54,7 @@ static int header_check_orf_IIRO(const unsigned char *buffer, const unsigned int
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_orf.extension;
file_recovery_new->time=get_date_from_tiff_header((const TIFFHeader *)buffer, buffer_size);
- file_recovery_new->file_check=&file_check_tiff;
+ file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/file_rw2.c b/src/file_rw2.c
index 1310561..4e2cd4f 100644
--- a/src/file_rw2.c
+++ b/src/file_rw2.c
@@ -53,7 +53,7 @@ static int header_check_rw2(const unsigned char *buffer, const unsigned int buff
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="rw2";
file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
- file_recovery_new->file_check=&file_check_tiff;
+ file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/file_tiff.c b/src/file_tiff.c
index 6dc113f..7599856 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -38,6 +38,9 @@
#include "common.h"
#include "file_tiff.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static void register_header_check_tiff(file_stat_t *file_stat);
@@ -138,10 +141,14 @@ const char *find_tag_from_tiff_header(const TIFFHeader *tiff, const unsigned int
{
if(tiff_size < sizeof(TIFFHeader))
return NULL;
+#ifndef MAIN_tiff_le
if(tiff->tiff_magic==TIFF_BIGENDIAN)
return find_tag_from_tiff_header_be(tiff, tiff_size, tag, potential_error);
- else if(tiff->tiff_magic==TIFF_LITTLEENDIAN)
+#endif
+#ifndef MAIN_tiff_be
+ if(tiff->tiff_magic==TIFF_LITTLEENDIAN)
return find_tag_from_tiff_header_le(tiff, tiff_size, tag, potential_error);
+#endif
return NULL;
}
@@ -165,43 +172,10 @@ static void register_header_check_tiff(file_stat_t *file_stat)
{
static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
+#ifndef MAIN_tiff_le
register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
+#endif
+#ifndef MAIN_tiff_be
register_header_check(0, tiff_header_le, sizeof(tiff_header_le), &header_check_tiff_le, file_stat);
-}
-
-void file_check_tiff(file_recovery_t *fr)
-{
- 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(header.tiff_magic==TIFF_LITTLEENDIAN)
- calculated_file_size=file_check_tiff_le(fr, le32(header.tiff_diroff), 0, 0);
- else if(header.tiff_magic==TIFF_BIGENDIAN)
- calculated_file_size=file_check_tiff_be(fr, be32(header.tiff_diroff), 0, 0);
-#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;
}
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
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index ffb6d4b..fb4eebc 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -42,8 +42,16 @@
#include "__fc_builtin.h"
#endif
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
extern const file_hint_t file_hint_jpg;
+#endif
+extern const file_hint_t file_hint_tiff;
+static const char *extension_dcr="dcr";
+static const char *extension_dng="dng";
+static const char *extension_nef="nef";
+static const char *extension_pef="pef";
+#ifndef MAIN_tiff_le
/*@
@ requires \valid_read((const unsigned char*)tiff+(0..tiff_size-1));
@ requires \valid(potential_error);
@@ -143,14 +151,22 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
be16(entry_strip_bytecounts->tdir_type)!=4)
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, be32(entry_strip_offsets->tdir_offset), SEEK_SET) < 0 ||
fread(offsetp, sizeof(*offsetp), nbr, handle) != nbr)
{
free(offsetp);
return TIFF_ERROR;
}
+#ifdef __FRAMAC__
+ sizep=(uint32_t *)MALLOC(2048*sizeof(*sizep));
+#else
sizep=(uint32_t *)MALLOC(nbr*sizeof(*sizep));
+#endif
if(fseek(handle, be32(entry_strip_bytecounts->tdir_offset), SEEK_SET) < 0 ||
fread(sizep, sizeof(*sizep), nbr, handle) != nbr)
{
@@ -158,9 +174,13 @@ static uint64_t parse_strip_be(FILE *handle, const TIFFDirEntry *entry_strip_off
free(sizep);
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=be32(offsetp[i]) + be32(sizep[i]);
+ const uint64_t tmp=(uint64_t)be32(offsetp[i]) + be32(sizep[i]);
if(max_offset < tmp)
max_offset=tmp;
}
@@ -217,6 +237,9 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
return TIFF_ERROR;
+#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 ||
@@ -289,7 +312,15 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
}
#endif
-uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
+#ifndef MAIN_tiff_le
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires valid_read_string(fr->extension);
+ @
+ */
+static uint64_t file_check_tiff_be_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;
@@ -313,7 +344,7 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
#ifdef DEBUG_TIFF
- log_info("file_check_tiff_be(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
+ log_info("file_check_tiff_be_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
if(depth>4)
return TIFF_ERROR;
@@ -334,13 +365,13 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
/*@ assert 2 <= data_read <= sizeof(buffer); */
n=(buffer[0]<<8)+buffer[1];
#ifdef DEBUG_TIFF
- log_info("file_check_tiff_be(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
+ log_info("file_check_tiff_be_aux(fr, %lu, %u, %u) => %u entries\n", (long unsigned)tiff_diroff, depth, count, n);
#endif
if(n==0)
return TIFF_ERROR;
/*@ assert sizeof(TIFFDirEntry)==12; */
/*@
- @ loop invariant 0 <= i <=n && i < (data_read-2)/12;
+ @ loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@ loop variant n-i;
@*/
for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
@@ -348,8 +379,9 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
const TIFFDirEntry *entry=&entries[i];
/*@ assert 0 <= i < n; */
/*@ assert \valid_read(entry); */
+ const unsigned int tdir_count=be32(entry->tdir_count);
const unsigned int tdir_tag=be16(entry->tdir_tag);
- const uint64_t val=(uint64_t)be32(entry->tdir_count) * tiff_type2size(be16(entry->tdir_type));
+ const uint64_t val=(uint64_t)tdir_count * tiff_type2size(be16(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,
@@ -357,7 +389,7 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
tdir_tag,
tag_name(tdir_tag),
be16(entry->tdir_type),
- (long unsigned)be32(entry->tdir_count),
+ (long unsigned)tdir_count,
(long unsigned)be32(entry->tdir_offset),
(long unsigned)be32(entry->tdir_offset),
(long unsigned)val);
@@ -379,7 +411,7 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
if(max_offset < new_offset)
max_offset=new_offset;
}
- if(be32(entry->tdir_count)==1 && val<=4)
+ if(tdir_count==1 && val<=4)
{
const unsigned int tmp=tiff_be_read(&entry->tdir_offset, be16(entry->tdir_type));
switch(tdir_tag)
@@ -396,22 +428,26 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
+#ifndef __FRAMAC__
{
- const uint64_t new_offset=file_check_tiff_be(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
+#endif
break;
case TIFFTAG_SUBIFD:
+#ifndef __FRAMAC__
{
- const uint64_t new_offset=file_check_tiff_be(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
+#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@@ -426,9 +462,9 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
#endif
}
}
- else if(be32(entry->tdir_count) > 1)
+ else if(tdir_count > 1)
{
- /*@ assert le32(entry->tdir_count) > 1; */
+ /*@ assert tdir_count > 1; */
switch(tdir_tag)
{
case TIFFTAG_EXIFIFD:
@@ -436,7 +472,7 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
case TIFFTAG_SUBIFD:
if(be16(entry->tdir_type)==4)
{
- const unsigned int nbr=(be32(entry->tdir_count)<32?be32(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;
@@ -451,13 +487,14 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
#endif
+#ifndef __FRAMAC__
/*@
@ loop invariant 0 <= j <= nbr <=32;
@ loop variant nbr-j;
@*/
for(j=0; j<nbr; j++)
{
- const uint64_t new_offset=file_check_tiff_be(fr, be32(subifd_offsetp[j]), depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(subifd_offsetp[j]), depth+1, 0);
if(new_offset==TIFF_ERROR)
{
return TIFF_ERROR;
@@ -465,6 +502,7 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
if(max_offset < new_offset)
max_offset = new_offset;
}
+#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -511,38 +549,94 @@ uint64_t file_check_tiff_be(file_recovery_t *fr, const uint32_t tiff_diroff, con
if(max_offset < tmp)
max_offset=tmp;
}
+#ifndef __FRAMAC__
if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
/*@ assert n <= (data_read - 6) /12; */
const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n];
if(be32(*tiff_next_diroff) > 0)
{
- const uint64_t new_offset=file_check_tiff_be(fr, be32(*tiff_next_diroff), depth+1, count+1);
+ const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(*tiff_next_diroff), depth+1, count+1);
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
}
+#endif
return max_offset;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires valid_read_string(fr->extension);
+ @*/
+static void file_check_tiff_be(file_recovery_t *fr)
+{
+ 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_BIGENDIAN)
+ calculated_file_size=file_check_tiff_be_aux(fr, be32(header.tiff_diroff), 0, 0);
+#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
+
+/*@
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_tiff.extension ||
+ file_recovery_new->extension == extension_dcr ||
+ file_recovery_new->extension == extension_dng ||
+ file_recovery_new->extension == extension_nef ||
+ file_recovery_new->extension == extension_pef);
+ @*/
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)
{
const char *potential_error=NULL;
const TIFFHeader *header=(const TIFFHeader *)buffer;
if((uint32_t)be32(header->tiff_diroff) < sizeof(TIFFHeader))
return 0;
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
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;
if(find_tag_from_tiff_header_be(header, buffer_size, TIFFTAG_DNGVERSION, &potential_error)!=NULL)
{
/* Adobe Digital Negative, ie. PENTAX K-30 */
- file_recovery_new->extension="dng";
+ file_recovery_new->extension=extension_dng;
}
else
{
@@ -552,14 +646,15 @@ int header_check_tiff_be(const unsigned char *buffer, const unsigned int buffer_
{
if( memcmp(tag_make, "PENTAX Corporation ", 20)==0 ||
memcmp(tag_make, "PENTAX ", 20)==0)
- file_recovery_new->extension="pef";
+ file_recovery_new->extension=extension_pef;
else if(memcmp(tag_make, "NIKON CORPORATION", 18)==0)
- file_recovery_new->extension="nef";
+ file_recovery_new->extension=extension_nef;
else if(memcmp(tag_make, "Kodak", 6)==0)
- file_recovery_new->extension="dcr";
+ file_recovery_new->extension=extension_dcr;
}
}
file_recovery_new->time=get_date_from_tiff_header(header, buffer_size);
- file_recovery_new->file_check=&file_check_tiff;
+ file_recovery_new->file_check=&file_check_tiff_be;
return 1;
}
+#endif
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index fb62732..899e342 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -42,9 +42,19 @@
#include "__fc_builtin.h"
#endif
+#if !defined(MAIN_tiff_be) && !defined(MAIN_tiff_le)
extern const file_hint_t file_hint_raf;
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";
+
+#ifndef MAIN_tiff_be
/*@
@ requires \valid_read((const unsigned char*)tiff+(0..tiff_size-1));
@ requires \valid(potential_error);
@@ -144,14 +154,22 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
le16(entry_strip_bytecounts->tdir_type)!=4)
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 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)
{
@@ -159,9 +177,13 @@ static uint64_t parse_strip_le(FILE *handle, const TIFFDirEntry *entry_strip_off
free(sizep);
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;
}
@@ -218,6 +240,9 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
data_read=fread(buffer, 1, sizeof(buffer), in);
if(data_read<2)
return TIFF_ERROR;
+#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 ||
@@ -290,7 +315,15 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
}
#endif
-uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
+#ifndef MAIN_tiff_be
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid_read(&fr->extension);
+ @ requires 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;
@@ -314,7 +347,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
const TIFFDirEntry *entry_tile_offsets=NULL;
const TIFFDirEntry *entry_tile_bytecounts=NULL;
#ifdef DEBUG_TIFF
- log_info("file_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 TIFF_ERROR;
@@ -335,13 +368,13 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
/*@ assert 2 <= data_read <= sizeof(buffer); */
n=buffer[0] | (buffer[1]<<8);
#ifdef DEBUG_TIFF
- log_info("file_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
if(n==0)
return TIFF_ERROR;
/*@ assert sizeof(TIFFDirEntry)==12; */
/*@
- @ loop invariant 0 <= i <=n && i < (data_read-2)/12;
+ @ loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@ loop variant n-i;
@*/
for(i=0; i < n && i < (unsigned int)(data_read-2)/12; i++)
@@ -349,8 +382,9 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
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,
@@ -358,7 +392,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
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);
@@ -367,7 +401,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
{ /* Entries must be sorted by tag, some SR2 files don't respect this rule */
if(sorted_tag_error > 0)
{
- if(strcmp(fr->extension,"sr2")!=0)
+ if(fr->extension != extension_sr2)
return TIFF_ERROR;
}
else
@@ -381,7 +415,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
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)
@@ -398,29 +432,33 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
+#ifndef __FRAMAC__
{
- const uint64_t new_offset=file_check_tiff_le(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
+#endif
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)
max_offset=tmp;
}
+#ifndef __FRAMAC__
else
{
- const uint64_t new_offset=file_check_tiff_le(fr, tmp, depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, tmp, depth+1, 0);
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
if(max_offset < new_offset)
max_offset=new_offset;
}
+#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@@ -435,9 +473,9 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
#endif
}
}
- else if(le32(entry->tdir_count) > 1)
+ else if(tdir_count > 1)
{
- /*@ assert le32(entry->tdir_count) > 1; */
+ /*@ assert tdir_count > 1; */
switch(tdir_tag)
{
case TIFFTAG_EXIFIFD:
@@ -445,7 +483,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
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;
@@ -460,13 +498,14 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)&subifd_offsetp, sizeof(subifd_offsetp));
#endif
+#ifndef __FRAMAC__
/*@
@ loop invariant 0 <= j <= nbr <=32;
@ loop variant nbr-j;
@*/
for(j=0; j<nbr; j++)
{
- const uint64_t new_offset=file_check_tiff_le(fr, le32(subifd_offsetp[j]), depth+1, 0);
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(subifd_offsetp[j]), depth+1, 0);
if(new_offset==TIFF_ERROR)
{
return TIFF_ERROR;
@@ -474,6 +513,7 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
if(max_offset < new_offset)
max_offset = new_offset;
}
+#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -520,20 +560,69 @@ uint64_t file_check_tiff_le(file_recovery_t *fr, const uint32_t tiff_diroff, con
if(max_offset < tmp)
max_offset=tmp;
}
+#ifndef __FRAMAC__
if ( 2 + n*12 + 4 <= (unsigned int)data_read)
{
/*@ assert n <= (data_read - 6) /12; */
const uint32_t *tiff_next_diroff=(const uint32_t *)&entries[n];
if(le32(*tiff_next_diroff) > 0)
{
- const uint64_t new_offset=file_check_tiff_le(fr, le32(*tiff_next_diroff), depth+1, count+1);
+ const uint64_t new_offset=file_check_tiff_le_aux(fr, le32(*tiff_next_diroff), depth+1, count+1);
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
}
+#endif
return max_offset;
}
+void file_check_tiff_le(file_recovery_t *fr)
+{
+ 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);
+#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
+
+/*@
+ @ 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};
@@ -543,27 +632,31 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
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)
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)
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";
+ file_recovery_new->extension=extension_cr2;
else if(find_tag_from_tiff_header_le(header, buffer_size, TIFFTAG_DNGVERSION, &potential_error)!=NULL)
{
/* Adobe Digital Negative, ie. NIKON D50 */
- file_recovery_new->extension="dng";
+ file_recovery_new->extension=extension_dng;
}
else
{
@@ -575,14 +668,91 @@ int header_check_tiff_le(const unsigned char *buffer, const unsigned int buffer_
* sr2 if Sony::FileFormat begins by 1
* arw otherwise */
if(memcmp(tag_make, "SONY", 5)==0)
- file_recovery_new->extension="sr2";
+ file_recovery_new->extension=extension_sr2;
else if(strncmp(tag_make, "SONY ",5)==0)
- file_recovery_new->extension="arw";
+ file_recovery_new->extension=extension_arw;
else if(tag_make < (const char *)buffer + buffer_size - 18 && memcmp(tag_make, "NIKON CORPORATION", 18)==0)
- file_recovery_new->extension="nef";
+ 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->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
diff --git a/src/file_wdp.c b/src/file_wdp.c
index 7948cc6..f70dd56 100644
--- a/src/file_wdp.c
+++ b/src/file_wdp.c
@@ -52,7 +52,7 @@ static int header_check_wdp(const unsigned char *buffer, const unsigned int buff
reset_file_recovery(file_recovery_new);
file_recovery_new->extension="wdp";
file_recovery_new->time=get_date_from_tiff_header((const TIFFHeader *)buffer, buffer_size);
- file_recovery_new->file_check=&file_check_tiff;
+ file_recovery_new->file_check=&file_check_tiff_le;
return 1;
}
diff --git a/src/filegen.h b/src/filegen.h
index 1e2fb4e..70cbee4 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -251,6 +251,7 @@ void header_ignored(const file_recovery_t *file_recovery_new);
/*@
@ requires \valid_read(file_recovery);
@ requires \valid_read(file_recovery_new);
+ @ requires separation: \separated(file_recovery, file_recovery_new);
@ requires \initialized(&file_recovery->file_check);
@ requires \initialized(&file_recovery->handle);
@ ensures \result == 0 || \result == 1;