summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-11-23 18:30:36 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-11-23 18:30:36 +0100
commitb310abea46850c846c9df6cac089976c23191301 (patch)
tree265895db5165411fc78affe20b84feaf739d5da4 /src
parent7e8f99aa92038220efa4d9c45cf8a0857a77d7d8 (diff)
src/file_jpg.c: make most code frama-c friendly, file_tiff* modified to help
Diffstat (limited to 'src')
-rw-r--r--src/file_jpg.c324
-rw-r--r--src/file_tiff.c9
-rw-r--r--src/file_tiff.h1
-rw-r--r--src/file_tiff_be.c111
-rw-r--r--src/file_tiff_le.c109
5 files changed, 349 insertions, 205 deletions
diff --git a/src/file_jpg.c b/src/file_jpg.c
index 3b0a895..64abd7b 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -288,7 +288,6 @@ static uint64_t check_mpo_le(const unsigned char *mpo, const uint64_t mpo_offset
@*/
static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const unsigned int size)
{
-#ifndef MAIN_jpg
if(mpo[0]=='I' && mpo[1]=='I' && mpo[2]=='*' && mpo[3]==0)
{
return check_mpo_le(mpo, offset, size);
@@ -297,13 +296,13 @@ static uint64_t check_mpo(const unsigned char *mpo, const uint64_t offset, const
{
return check_mpo_be(mpo, offset, size);
}
-#endif
return 0;
}
/*@
@ requires \valid(fr);
@ requires \valid(fr->handle);
+ @ requires valid_read_string((char *)&fr->filename);
@ requires \initialized(&fr->time);
@*/
static void file_check_mpo(file_recovery_t *fr)
@@ -402,8 +401,36 @@ static int is_marker_valid(const unsigned int marker)
}
/*@
+ @ requires \valid_read(buffer + (0 .. buffer_size-1));
+ @*/
+static time_t jpg_get_date(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int i, const unsigned int size)
+{ /* APP1 Exif information */
+ const unsigned int tiff_offset=i+2+8;
+ if(tiff_offset < buffer_size && size > 8)
+ {
+ /*@ assert tiff_offset < buffer_size; */
+ /*@ assert size > 8; */
+ unsigned int tiff_size=size-0x08;
+ if(buffer_size - tiff_offset < tiff_size)
+ {
+ tiff_size=buffer_size - tiff_offset;
+ /*@ assert tiff_offset + tiff_size == buffer_size; */
+ }
+ else
+ {
+ /*@ assert tiff_offset + tiff_size <= buffer_size; */
+ }
+ /*@ assert tiff_offset + tiff_size <= buffer_size; */
+ return get_date_from_tiff_header(&buffer[tiff_offset], tiff_size);
+ }
+ return 0;
+}
+
+
+/*@
@ 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;
@@ -530,22 +557,14 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
}
while(i+4<buffer_size && buffer[i]==0xff && is_marker_valid(buffer[i+1]))
{
+ const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
if(buffer[i+1]==0xff)
i++;
else
{
if(buffer[i+1]==0xe1)
{ /* APP1 Exif information */
- const unsigned int tmp=2+(buffer[i+2]<<8)+buffer[i+3];
- if(i+0x0A < buffer_size && tmp > 0x0A)
- {
- unsigned int tiff_size=tmp-0x0A;
- if(buffer_size - (i+0x0A) < tiff_size)
- tiff_size=buffer_size - (i+0x0A);
-#ifndef MAIN_jpg
- jpg_time=get_date_from_tiff_header(&buffer[i+0x0A], tiff_size);
-#endif
- }
+ jpg_time=jpg_get_date(buffer, buffer_size, i, size);
}
else if(buffer[i+1]==0xc4)
{
@@ -553,7 +572,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
if(jpg_check_dht(buffer, buffer_size, i, 2+(buffer[i+2]<<8)+buffer[i+3])!=0)
return 0;
}
- i+=2+(buffer[i+2]<<8)+buffer[i+3];
+ i+=2+size;
}
}
if(i+1 < file_recovery_new->blocksize && buffer[i+1]!=0xda)
@@ -572,8 +591,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
return 1;
}
-#ifndef MAIN_jpg
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
struct my_error_mgr {
struct jpeg_error_mgr pub; /* "public" fields, must be the first field */
@@ -1378,7 +1396,6 @@ static void jpg_check_picture(file_recovery_t *file_recovery)
}
}
#endif
-#endif
/*@
@ requires i < buffer_size;
@@ -1461,6 +1478,7 @@ static int jpg_check_sof0(const unsigned char *buffer, const unsigned int buffer
@ requires \valid(file_recovery->handle);
@ requires file_recovery->blocksize <= 1048576;
@ requires file_recovery->offset_error <= (1<<63) - 1;
+ @ ensures \valid(file_recovery->handle);
@*/
static void jpg_search_marker(file_recovery_t *file_recovery)
{
@@ -1498,6 +1516,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
@ loop invariant offset + i >= offset_test;
@ loop invariant offset_test >= file_recovery->offset_error;
@ loop invariant 0 <= i < nbytes + file_recovery->blocksize;
+ @ loop assigns i,file_recovery->extra;
@*/
while(i+1<nbytes)
{
@@ -1514,12 +1533,14 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
)
{
file_recovery->extra=tmp - file_recovery->offset_error;
+#ifndef __FRAMAC__
if(file_recovery->extra % file_recovery->blocksize != 0)
{
log_info("jpg_search_marker %s extra=%llu\n",
file_recovery->filename,
(long long unsigned)file_recovery->extra);
}
+#endif
return ;
}
i+=file_recovery->blocksize;
@@ -1533,6 +1554,7 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
@ requires \valid(thumb_offset);
+ @ requires valid_read_string((char *)&file_recovery->filename);
@ requires file_recovery->blocksize > 0;
@ requires \valid_read(buffer + (0 .. nbytes-1));
@ requires \initialized(&file_recovery->time);
@@ -1541,158 +1563,158 @@ static void jpg_search_marker(file_recovery_t *file_recovery)
static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int extract_thumb, const unsigned char *buffer, const unsigned int i, const unsigned int offset, const unsigned int size, const size_t nbytes, uint64_t *thumb_offset)
{ /* APP1 Exif information */
const unsigned int tiff_offset=i+2+8;
- if(tiff_offset < nbytes && size > 8)
+ const unsigned char *potential_error=NULL;
+ const unsigned char *thumb_data=NULL;
+ const unsigned char *tiff;
+ unsigned int thumb_size=0;
+ unsigned int tiff_size;
+ if(tiff_offset >= nbytes || size <= 8)
+ return 1;
+ /*@ assert tiff_offset < nbytes; */
+ /*@ assert size > 8; */
+ tiff_size=size-0x08;
+ if(nbytes - tiff_offset < tiff_size)
{
- /*@ assert tiff_offset < nbytes; */
- /*@ assert size > 8; */
- const unsigned char *potential_error=NULL;
- unsigned int tiff_size=size-0x08;
- const unsigned char *thumb_data=NULL;
- unsigned int thumb_size=0;
- if(nbytes - tiff_offset < tiff_size)
+ tiff_size=nbytes - tiff_offset;
+ /*@ assert tiff_offset + tiff_size == nbytes; */
+ }
+ else
+ {
+ /*@ assert tiff_offset + tiff_size <= nbytes; */
+ }
+ /*@ assert tiff_offset + tiff_size <= nbytes; */
+ if(tiff_size<sizeof(TIFFHeader))
+ return 1;
+ /*@ assert tiff_size >= sizeof(TIFFHeader); */
+ /*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */
+ /*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */
+ tiff=&buffer[tiff_offset];
+ /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
+ if(file_recovery->time==0)
+ {
+ /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
+ file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
+ }
+ *thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
+ if(*thumb_offset!=0)
+ {
+ *thumb_offset+=tiff_offset;
+ thumb_data=buffer+ (*thumb_offset);
+ thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
+ }
+ if(potential_error!=NULL)
+ {
+ file_recovery->offset_error=potential_error-buffer;
+ return 0;
+ }
+ if(file_recovery->offset_ok<i)
+ file_recovery->offset_ok=i;
+ if(thumb_data!=0 && thumb_size!=0 && *thumb_offset < nbytes - 1)
+ {
+ unsigned int j=*thumb_offset+2;
+ unsigned int thumb_sos_found=0;
+#ifdef DEBUG_JPEG
+ unsigned int j_old=j;
+#endif
+ if(buffer[*thumb_offset]!=0xff)
{
- tiff_size=nbytes - tiff_offset;
- /*@ assert tiff_offset + tiff_size == nbytes; */
+ file_recovery->offset_error=*thumb_offset;
+ jpg_search_marker(file_recovery);
+ return 0;
}
- else
+ if(buffer[*thumb_offset+1]!=0xd8)
{
- /*@ assert tiff_offset + tiff_size <= nbytes; */
+ file_recovery->offset_error=*thumb_offset+1;
+ return 0;
}
- /*@ assert tiff_offset + tiff_size <= nbytes; */
- if(tiff_size<sizeof(TIFFHeader))
- return 1;
- /*@ assert tiff_size >= sizeof(TIFFHeader); */
+ while(j+4<nbytes && thumb_sos_found==0)
{
- /*@ assert \valid_read(buffer + (0 .. tiff_offset+tiff_size-1)); */
- /*@ assert \valid_read((buffer + tiff_offset) + (0 .. tiff_size-1)); */
- const unsigned char *tiff=&buffer[tiff_offset];
- /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
- if(file_recovery->time==0)
+ if(buffer[j]!=0xff)
{
- /*@ assert \valid_read(tiff+ (0 .. tiff_size-1)); */
- file_recovery->time=get_date_from_tiff_header(tiff, tiff_size);
+ file_recovery->offset_error=j;
+#ifdef DEBUG_JPEG
+ log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
+ log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
+#endif
+ jpg_search_marker(file_recovery);
+ return 0;
}
-#ifndef __FRAMAC__
- *thumb_offset=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFOFFSET, &potential_error);
- if(*thumb_offset!=0)
+ if(buffer[j+1]==0xff)
{
- *thumb_offset+=tiff_offset;
- thumb_data=buffer+ (*thumb_offset);
- thumb_size=find_tag_from_tiff_header(tiff, tiff_size, TIFFTAG_JPEGIFBYTECOUNT, &potential_error);
+ /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
+ j++;
+ continue;
}
+#ifdef DEBUG_JPEG
+ log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
#endif
- if(potential_error!=NULL)
+ if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
+ thumb_sos_found=1;
+ else if(buffer[j+1]==0xc4) /* DHT */
{
- file_recovery->offset_error=potential_error-buffer;
- return 0;
+ if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
+ {
+ file_recovery->offset_error=j+2;
+ return 0;
+ }
}
- if(file_recovery->offset_ok<i)
- file_recovery->offset_ok=i;
-#ifndef MAIN_jpg
- if(thumb_data!=0 && thumb_size!=0)
+ else if(buffer[j+1]==0xdb || /* DQT */
+ buffer[j+1]==0xc0 || /* SOF0 */
+ buffer[j+1]==0xdd) /* DRI */
{
- if(*thumb_offset < nbytes - 1)
- {
- unsigned int j=*thumb_offset+2;
- unsigned int thumb_sos_found=0;
+ }
+ else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
+ (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
+ buffer[j+1]==0xfe) /* COM */
+ {
+ /* Unusual marker, bug ? */
+ }
+ else
+ {
+ log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
+ file_recovery->offset_error=j;
+ return 0;
+ }
+ if(file_recovery->offset_ok<j)
+ file_recovery->offset_ok=j;
#ifdef DEBUG_JPEG
- unsigned int j_old=j;
+ j_old=j;
#endif
- if(buffer[*thumb_offset]!=0xff)
- {
- file_recovery->offset_error=*thumb_offset;
- jpg_search_marker(file_recovery);
- return 0;
- }
- if(buffer[*thumb_offset+1]!=0xd8)
- {
- file_recovery->offset_error=*thumb_offset+1;
- return 0;
- }
- while(j+4<nbytes && thumb_sos_found==0)
+ j+=2U+(buffer[j+2]<<8)+buffer[j+3];
+ }
+ if(thumb_sos_found>0 && extract_thumb>0
+ && offset < nbytes && buffer[offset]==0xff)
+ {
+ char *thumbname;
+ /*@ assert valid_read_string((char *)&file_recovery->filename); */
+#ifndef __FRAMAC__
+ thumbname=strdup(file_recovery->filename);
+ if(thumbname!=NULL)
+ {
+ char *sep;
+ /*@ assert thumbname!=\null; */
+ /*@ assert valid_read_string(thumbname); */
+ sep=strrchr(thumbname,'/');
+ if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes)
+ {
+ FILE *out;
+ *(sep+1)='t';
+ if((out=fopen(thumbname,"wb"))!=NULL)
{
- if(buffer[j]!=0xff)
- {
- file_recovery->offset_error=j;
-#ifdef DEBUG_JPEG
- log_info("%s thumb no marker at 0x%x\n", file_recovery->filename, j);
- log_error("%s Error between %u and %u\n", file_recovery->filename, j_old, j);
-#endif
- jpg_search_marker(file_recovery);
- return 0;
- }
- if(buffer[j+1]==0xff)
+ if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1)
{
- /* See B.1.1.2 Markers in http://www.w3.org/Graphics/JPEG/itu-t81.pdf*/
- j++;
- continue;
+ log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
}
-#ifdef DEBUG_JPEG
- log_info("%s thumb marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
-#endif
- if(buffer[j+1]==0xda) /* Thumb SOS: Start Of Scan */
- thumb_sos_found=1;
- else if(buffer[j+1]==0xc4) /* DHT */
- {
- if(jpg_check_dht(buffer, nbytes, j, 2+(buffer[j+2]<<8)+buffer[j+3])!=0)
- {
- file_recovery->offset_error=j+2;
- return 0;
- }
- }
- else if(buffer[j+1]==0xdb || /* DQT */
- buffer[j+1]==0xc0 || /* SOF0 */
- buffer[j+1]==0xdd) /* DRI */
- {
- }
- else if((buffer[j+1]>=0xc0 && buffer[j+1]<=0xcf) || /* SOF0 - SOF15 */
- (buffer[j+1]>=0xe0 && buffer[j+1]<=0xef) || /* APP0 - APP15 */
- buffer[j+1]==0xfe) /* COM */
- {
- /* Unusual marker, bug ? */
- }
- else
- {
- log_info("%s thumb unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[j+1], j);
- file_recovery->offset_error=j;
- return 0;
- }
- if(file_recovery->offset_ok<j)
- file_recovery->offset_ok=j;
-#ifdef DEBUG_JPEG
- j_old=j;
-#endif
- j+=2U+(buffer[j+2]<<8)+buffer[j+3];
+ fclose(out);
+ if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
+ set_date(thumbname, file_recovery->time, file_recovery->time);
}
- if(thumb_sos_found>0 && extract_thumb>0
- && offset < nbytes && buffer[offset]==0xff)
+ else
{
- char *thumbname;
- char *sep;
- thumbname=strdup(file_recovery->filename);
- sep=strrchr(thumbname,'/');
- if(sep!=NULL && *(sep+1)=='f' && *thumb_offset+thumb_size < nbytes)
- {
- FILE *out;
- *(sep+1)='t';
- if((out=fopen(thumbname,"wb"))!=NULL)
- {
- if(fwrite(&buffer[*thumb_offset], thumb_size, 1, out) < 1)
- {
- log_error("Can't write to %s: %s\n", thumbname, strerror(errno));
- }
- fclose(out);
- if(file_recovery->time!=0 && file_recovery->time!=(time_t)-1)
- set_date(thumbname, file_recovery->time, file_recovery->time);
- }
- else
- {
- log_error("fopen %s failed\n", thumbname);
- }
- }
- free(thumbname);
+ log_error("fopen %s failed\n", thumbname);
}
}
+ free(thumbname);
}
#endif
}
@@ -1705,6 +1727,7 @@ static int jpg_check_app1(file_recovery_t *file_recovery, const unsigned int ext
@ requires \valid(file_recovery->handle);
@ requires file_recovery->blocksize > 0;
@ requires \initialized(&file_recovery->time);
+ @ requires valid_read_string((char *)&file_recovery->filename);
*/
static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsigned int extract_thumb)
{
@@ -1740,7 +1763,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
if(buffer[i]!=0xff)
{
-#ifdef DEBUG_JPEG
+#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
log_info("%s no marker at 0x%x\n", file_recovery->filename, i);
#endif
file_recovery->offset_error=i;
@@ -1753,7 +1776,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
offset++;
continue;
}
-#ifdef DEBUG_JPEG
+#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i);
#endif
offset+=(uint64_t)2+size;
@@ -1788,7 +1811,9 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
}
else
{
+#ifndef __FRAMAC__
log_info("%s unknown marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i+1);
+#endif
file_recovery->offset_error=i+1;
return thumb_offset;
}
@@ -1804,6 +1829,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
+ @ requires valid_read_string((char *)&file_recovery->filename);
@ requires \initialized(&file_recovery->time);
@*/
static void file_check_jpg(file_recovery_t *file_recovery)
@@ -1828,7 +1854,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#ifdef DEBUG_JPEG
log_info("jpg_check_structure error at %llu\n", (long long unsigned)file_recovery->offset_error);
#endif
-#ifndef MAIN_jpg
+#ifndef __FRAMAC__
#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
if(thumb_offset!=0 &&
(file_recovery->checkpoint_status==0 || thumb_error!=0) &&
@@ -1857,7 +1883,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
#endif
if(file_recovery->offset_error!=0)
return ;
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(MAIN_jpg)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(__FRAMAC__)
jpg_check_picture(file_recovery);
#else
file_recovery->file_size=file_recovery->calculated_file_size;
diff --git a/src/file_tiff.c b/src/file_tiff.c
index 0262457..96626ce 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -140,8 +140,11 @@ const char *tag_name(unsigned int tag)
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)
{
const TIFFHeader *tiff=(const TIFFHeader *)buffer;
- if(buffer_size < sizeof(TIFFHeader))
+ /*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */
+ if(buffer_size < sizeof(struct ifd_header))
return 0;
+ /*@ assert buffer_size >= sizeof(TIFFHeader); */
+ /*@ assert buffer_size >= sizeof(struct ifd_header); */
#ifndef MAIN_tiff_le
if(tiff->tiff_magic==TIFF_BIGENDIAN)
return find_tag_from_tiff_header_be(buffer, buffer_size, tag, potential_error);
@@ -159,9 +162,11 @@ time_t get_date_from_tiff_header(const unsigned char *buffer, const unsigned int
unsigned int date_asc=0;
time_t tmp;
/*@ assert \valid_read(buffer+(0..buffer_size-1)); */
- if(buffer_size < sizeof(TIFFHeader) || buffer_size < 19)
+ /*@ assert sizeof(TIFFHeader) <= sizeof(struct ifd_header); */
+ if(buffer_size < sizeof(struct ifd_header) || buffer_size < 19)
return (time_t)0;
/*@ assert buffer_size >= sizeof(TIFFHeader); */
+ /*@ assert buffer_size >= sizeof(struct ifd_header); */
/* DateTimeOriginal */
date_asc=find_tag_from_tiff_header(buffer, buffer_size, 0x9003, &potential_error);
/* DateTimeDigitalized*/
diff --git a/src/file_tiff.h b/src/file_tiff.h
index b030da2..0fb5f6c 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -69,7 +69,6 @@ struct ifd_header {
} __attribute__ ((gcc_struct, __packed__));
/*@
- @ requires buffer_size >= sizeof(TIFFHeader);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ ensures \valid_read(buffer+(0..buffer_size-1));
@*/
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index 21bfd5f..92ac870 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -126,7 +126,7 @@ unsigned int find_tag_from_tiff_header_be(const unsigned char *buffer, const uns
return 0;
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
/*@ assert offset_ifd0 + sizeof(struct ifd_header) <= tiff_size; */
- /*@ assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */
+ /*X assert \valid_read(buffer+(0..offset_ifd0 + sizeof(struct ifd_header)-1)); */
{
const unsigned int tmp=find_tag_from_tiff_header_be_aux(buffer, tiff_size, tag, potential_error, offset_ifd0);
/*@ assert \valid_read(buffer+(0..tiff_size-1)); */
@@ -259,6 +259,7 @@ 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;
+ /*@ assert data_read >= 2; */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
@@ -336,16 +337,55 @@ static uint64_t tiff_be_makernote(FILE *in, const uint32_t tiff_diroff)
#endif
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
+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_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_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_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_be_aux(file_recovery_t *fr, const uint32_t tiff_diroff, const unsigned int depth, const unsigned int count)
{
unsigned char buffer[8192];
@@ -369,6 +409,9 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
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("file_check_tiff_be_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
@@ -395,6 +438,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(n==0)
return TIFF_ERROR;
+ /*@ assert 0 < n <= 65535; */
/*@ assert sizeof(TIFFDirEntry)==12; */
/*X
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@@ -402,6 +446,10 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
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); */
@@ -454,28 +502,38 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
-#ifndef __FRAMAC__
{
+ /*@ 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_be_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;
}
-#endif
break;
case TIFFTAG_SUBIFD:
-#ifndef __FRAMAC__
{
+ /*@ 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_be_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;
}
-#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@@ -515,15 +573,21 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
#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;
- @*/
+ /*X
+ X loop invariant 0 <= j <= nbr <=32;
+ X loop variant nbr-j;
+ X*/
for(j=0; j<nbr; j++)
{
+ /*@ 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_be_aux(fr, be32(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)
{
return TIFF_ERROR;
@@ -531,7 +595,6 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < new_offset)
max_offset = new_offset;
}
-#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -578,22 +641,16 @@ 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 < 6)
- return max_offset;
- /*@ assert data_read >= 6; */
-#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_aux(fr, be32(*tiff_next_diroff), depth+1, count+1);
- if(new_offset != TIFF_ERROR && max_offset < new_offset)
- max_offset=new_offset;
- }
+ const unsigned int offset_ptr_offset=2+12*n;
+ const uint64_t new_offset=file_check_tiff_be_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;
}
-#endif
return max_offset;
}
diff --git a/src/file_tiff_le.c b/src/file_tiff_le.c
index 5b20565..590e7bf 100644
--- a/src/file_tiff_le.c
+++ b/src/file_tiff_le.c
@@ -262,6 +262,7 @@ 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;
+ /*@ assert data_read >= 2; */
#if defined(__FRAMAC__)
Frama_C_make_unknown((char *)buffer, sizeof(buffer));
#endif
@@ -339,16 +340,55 @@ static uint64_t tiff_le_makernote(FILE *in, const uint32_t tiff_diroff)
#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);
+
/*@
@ 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];
@@ -372,6 +412,9 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
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("file_check_tiff_le_aux(fr, %lu, %u, %u)\n", (long unsigned)tiff_diroff, depth, count);
#endif
@@ -398,6 +441,7 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#endif
if(n==0)
return TIFF_ERROR;
+ /*@ assert 0 < n <= 65535; */
/*@ assert sizeof(TIFFDirEntry)==12; */
/*X
X loop invariant 0 <= i <=n && i <= (data_read-2)/12;
@@ -405,6 +449,10 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
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); */
@@ -458,16 +506,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
case TIFFTAG_TILEOFFSETS: tile_offsets=tmp; break;
case TIFFTAG_EXIFIFD:
case TIFFTAG_KODAKIFD:
-#ifndef __FRAMAC__
{
+ /*@ 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;
}
-#endif
break;
case TIFFTAG_SUBIFD:
if(fr->extension == extension_arw)
@@ -476,17 +529,22 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < tmp)
max_offset=tmp;
}
-#ifndef __FRAMAC__
else
{
+ /*@ 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;
}
-#endif
break;
#ifdef ENABLE_TIFF_MAKERNOTE
case EXIFTAG_MAKERNOTE:
@@ -526,15 +584,21 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
#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;
- @*/
+ /*X
+ X loop invariant 0 <= j <= nbr <=32;
+ X loop variant nbr-j;
+ X*/
for(j=0; j<nbr; j++)
{
+ /*@ 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)
{
return TIFF_ERROR;
@@ -542,7 +606,6 @@ static uint64_t file_check_tiff_le_aux(file_recovery_t *fr, const uint32_t tiff_
if(max_offset < new_offset)
max_offset = new_offset;
}
-#endif
}
break;
case TIFFTAG_STRIPOFFSETS:
@@ -589,22 +652,16 @@ 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 < 6)
- return max_offset;
- /*@ assert data_read >= 6; */
-#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_aux(fr, le32(*tiff_next_diroff), depth+1, count+1);
- if(new_offset != TIFF_ERROR && max_offset < new_offset)
- 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;
}
-#endif
return max_offset;
}