summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/file_tiff_be.c121
-rw-r--r--src/file_tiff_le.c121
-rw-r--r--src/filegen.h5
3 files changed, 90 insertions, 157 deletions
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index baeb6ee0..f33a514f 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -415,57 +415,12 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
-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);
-
-/*@
- @ requires \valid(fr);
- @ requires \valid(fr->handle);
- @ requires valid_file_recovery(fr);
- @ requires \valid_read(&fr->extension);
- @ requires valid_read_string(fr->extension);
- @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
- @ requires \valid_read(buffer + (0 .. buffer_size - 1));
- @ ensures \valid(fr);
- @ ensures \valid(fr->handle);
- @ ensures valid_read_string(fr->extension);
- @ assigns *fr->handle, errno;
- @ assigns Frama_C_entropy_source;
- @*/
-static uint64_t file_check_tiff_be_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=be32(*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_be_aux(fr, next_diroff, depth+1, count+1);
- }
-}
-
/*@
- @ requires \valid(fr);
- @ requires \valid(fr->handle);
- @ requires valid_file_recovery(fr);
- @ requires \valid_read(&fr->extension);
+ @ requires valid_file_check_param(fr);
@ requires valid_read_string(fr->extension);
- @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
- @ ensures \valid(fr);
- @ ensures \valid(fr->handle);
+ @ requires depth <= 5;
+ @ decreases 5 - depth;
+ @ ensures valid_file_check_param(fr);
@ ensures valid_read_string(fr->extension);
@ assigns *fr->handle, errno;
@ assigns Frama_C_entropy_source;
@@ -504,8 +459,10 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(depth>4)
return TIFF_ERROR;
+ /*@ assert depth <= 4; */
if(count>16)
return TIFF_ERROR;
+ /*@ assert count <= 16; */
if(tiff_diroff < sizeof(TIFFHeader))
return TIFF_ERROR;
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
@@ -531,8 +488,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
X*/
/*@
- @ loop invariant valid_file_recovery(fr);
- @ loop invariant \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
+ @ loop invariant valid_file_check_param(fr);
@ loop assigns *fr->handle, errno;
@ loop assigns Frama_C_entropy_source;
@ loop assigns i, sorted_tag_error, tdir_tag_old;
@@ -612,15 +568,11 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
{
- /*@ assert \valid(fr); */
- /*@ assert valid_file_recovery(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
@@ -630,15 +582,11 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
break;
case TIFFTAG_SUBIFD:
{
- /*@ assert \valid(fr); */
- /*@ assert valid_file_recovery(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
const uint64_t new_offset=file_check_tiff_be_aux(fr, tmp, depth+1, 0);
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
@@ -687,22 +635,20 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
Frama_C_make_unknown(&subifd_offsetp_buf, sizeof(subifd_offsetp_buf));
#endif
/*@
- @ loop invariant valid_file_recovery(fr);
- @ loop invariant \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
+ @ loop invariant valid_file_check_param(fr);
+ @ loop invariant \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ loop assigns *fr->handle, errno;
@ loop assigns Frama_C_entropy_source;
@ loop assigns j, max_offset;
+ @ loop variant nbr - j;
@*/
for(j=0; j<nbr; j++)
{
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
const uint64_t new_offset=file_check_tiff_be_aux(fr, be32(subifd_offsetp[j]), depth+1, 0);
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
{
@@ -757,13 +703,32 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
+ if(data_read < 4)
+ return max_offset;
+ /*@ assert data_read >= 4; */
{
const unsigned int offset_ptr_offset=2+12*n;
- const uint64_t new_offset=file_check_tiff_be_aux_next(fr, depth, count, ubuffer, data_read, offset_ptr_offset);
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
- /*@ assert valid_read_string(fr->extension); */
+ uint64_t new_offset;
+ if(offset_ptr_offset > data_read-4)
+ return max_offset;
+ /*@ assert offset_ptr_offset <= data_read - 4; */
+ /*@ assert offset_ptr_offset + 4 <= data_read; */
+ {
+ /*@ assert \valid_read(ubuffer + (0 .. offset_ptr_offset + 4 - 1)); */
+ const unsigned char *ptr_offset=&ubuffer[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=be32(*ptr32_offset);
+ if(next_diroff == 0)
+ return max_offset;
+ /*@ assert valid_file_check_param(fr); */
+ /*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
+ new_offset=file_check_tiff_be_aux(fr, next_diroff, depth+1, count+1);
+ /*@ assert valid_file_check_param(fr); */
+ /*@ assert valid_read_string(fr->extension); */
+ }
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 4d376013..2c697eea 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -416,57 +416,12 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#if !defined(MAIN_tiff_be) && !defined(MAIN_jpg) && !defined(SINGLE_FORMAT_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);
-
/*@
- @ requires \valid(fr);
- @ requires \valid(fr->handle);
- @ requires valid_file_recovery(fr);
- @ requires \valid_read(&fr->extension);
+ @ requires valid_file_check_param(fr);
@ requires valid_read_string(fr->extension);
- @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
- @ requires \valid_read(buffer + (0 .. buffer_size - 1));
- @ ensures \valid(fr);
- @ ensures \valid(fr->handle);
- @ ensures valid_read_string(fr->extension);
- @ assigns *fr->handle, errno;
- @ assigns Frama_C_entropy_source;
- @*/
-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_file_recovery(fr);
- @ requires \valid_read(&fr->extension);
- @ requires valid_read_string(fr->extension);
- @ requires separation: \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
- @ ensures \valid(fr);
- @ ensures \valid(fr->handle);
+ @ requires depth <= 5;
+ @ decreases 5 - depth;
+ @ ensures valid_file_check_param(fr);
@ ensures valid_read_string(fr->extension);
@ assigns *fr->handle, errno;
@ assigns Frama_C_entropy_source;
@@ -505,8 +460,10 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(depth>4)
return TIFF_ERROR;
+ /*@ assert depth <= 4; */
if(count>16)
return TIFF_ERROR;
+ /*@ assert count <= 16; */
if(tiff_diroff < sizeof(TIFFHeader))
return TIFF_ERROR;
if(fseek(fr->handle, tiff_diroff, SEEK_SET) < 0)
@@ -532,8 +489,8 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
X*/
/*@
- @ loop invariant valid_file_recovery(fr);
- @ loop invariant \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
+ @ loop invariant valid_file_check_param(fr);
+ @ loop invariant \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ loop assigns *fr->handle, errno;
@ loop assigns Frama_C_entropy_source;
@ loop assigns i, sorted_tag_error, tdir_tag_old;
@@ -614,15 +571,11 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
{
- /*@ assert \valid(fr); */
- /*@ assert valid_file_recovery(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
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_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
@@ -639,15 +592,11 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
}
else
{
- /*@ assert \valid(fr); */
- /*@ assert valid_file_recovery(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
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_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
return TIFF_ERROR;
@@ -696,8 +645,8 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
Frama_C_make_unknown(&subifd_offsetp_buf, sizeof(subifd_offsetp_buf));
#endif
/*@
- @ loop invariant valid_file_recovery(fr);
- @ loop invariant \separated(fr, fr->handle, &errno, &Frama_C_entropy_source);
+ @ loop invariant valid_file_check_param(fr);
+ @ loop invariant \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ loop assigns *fr->handle, errno;
@ loop assigns Frama_C_entropy_source;
@ loop assigns j, max_offset;
@@ -705,14 +654,11 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
@*/
for(j=0; j<nbr; j++)
{
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
+ /*@ assert valid_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
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_file_check_param(fr); */
/*@ assert valid_read_string(fr->extension); */
if(new_offset==TIFF_ERROR)
{
@@ -767,13 +713,32 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
+ if(data_read < 4)
+ return max_offset;
+ /*@ assert data_read >= 4; */
{
const unsigned int offset_ptr_offset=2+12*n;
- const uint64_t new_offset=file_check_tiff_le_aux_next(fr, depth, count, ubuffer, data_read, offset_ptr_offset);
- /*@ assert \valid(fr); */
- /*@ assert \valid(fr->handle); */
- /*@ assert \valid_read(&fr->extension); */
- /*@ assert valid_read_string(fr->extension); */
+ uint64_t new_offset;
+ if(offset_ptr_offset > data_read-4)
+ return max_offset;
+ /*@ assert offset_ptr_offset <= data_read - 4; */
+ /*@ assert offset_ptr_offset + 4 <= data_read; */
+ {
+ /*@ assert \valid_read(ubuffer + (0 .. offset_ptr_offset + 4 - 1)); */
+ const unsigned char *ptr_offset=&ubuffer[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 max_offset;
+ /*@ assert valid_file_check_param(fr); */
+ /*@ assert valid_read_string(fr->extension); */
+ /*@ assert depth <= 4; */
+ new_offset=file_check_tiff_le_aux(fr, next_diroff, depth+1, count+1);
+ /*@ assert valid_file_check_param(fr); */
+ /*@ assert valid_read_string(fr->extension); */
+ }
if(new_offset != TIFF_ERROR && max_offset < new_offset)
max_offset=new_offset;
}
diff --git a/src/filegen.h b/src/filegen.h
index 72813e58..c51ef7f4 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -195,8 +195,10 @@ typedef struct
);
predicate valid_file_check_result(file_recovery_t *file_recovery) = (
+ \valid(file_recovery) &&
+ \valid(file_recovery->handle) &&
valid_file_recovery(file_recovery) &&
- \valid(file_recovery->handle)
+ \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source)
);
predicate valid_data_check_param(unsigned char *buffer, unsigned int buffer_size, file_recovery_t *file_recovery) = (
@@ -388,6 +390,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable);
@ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
@ requires \separated(file_recovery, new_ext);
@ ensures valid_file_recovery(file_recovery);
+ @ ensures file_recovery->file_size == \old(file_recovery->file_size);
@*/
int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);