summaryrefslogtreecommitdiffstats
path: root/src/file_zip.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_zip.c')
-rw-r--r--src/file_zip.c877
1 files changed, 701 insertions, 176 deletions
diff --git a/src/file_zip.c b/src/file_zip.c
index ab25947..b6439cd 100644
--- a/src/file_zip.c
+++ b/src/file_zip.c
@@ -22,9 +22,6 @@
Information about ZIP file format: http://www.info-zip.org/doc/appnote-iz-latest.zip
*/
-/* Abolutely required for the zip64 stuff */
-/* #define _FILE_OFFSET_BITS 64 */
-
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@@ -39,15 +36,17 @@
#include "filegen.h"
#include "common.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
/* #define DEBUG_ZIP */
+#ifndef MAIN_zip
extern const file_hint_t file_hint_doc;
+#endif
static void register_header_check_zip(file_stat_t *file_stat);
-static int header_check_zip(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);
-static void file_check_zip(file_recovery_t *file_recovery);
static unsigned int pos_in_mem(const unsigned char *haystack, const unsigned int haystack_size, const unsigned char *needle, const unsigned int needle_size);
-static void file_rename_zip(file_recovery_t *file_recovery);
static char first_filename[256];
const file_hint_t file_hint_zip= {
@@ -59,6 +58,35 @@ const file_hint_t file_hint_zip= {
.register_header_check=&register_header_check_zip
};
+static const char *extension_apk="apk";
+static const char *extension_celtx="celtx";
+static const char *extension_docx="docx";
+static const char *extension_epub="epub";
+static const char *extension_jar="jar";
+static const char *extension_kmz="kmz";
+static const char *extension_kra="kra";
+static const char *extension_mmap="mmap";
+static const char *extension_notebook="notebook";
+static const char *extension_numbers="numbers";
+static const char *extension_odg="odg";
+static const char *extension_odp="odp";
+static const char *extension_ods="ods";
+static const char *extension_odt="odt";
+static const char *extension_ora="ora";
+static const char *extension_pages="pages";
+static const char *extension_pptx="pptx";
+static const char *extension_sh3d="sh3d";
+static const char *extension_sketch="sketch";
+static const char *extension_sxc="sxc";
+static const char *extension_sxd="sxd";
+static const char *extension_sxi="sxi";
+static const char *extension_sxw="sxw";
+static const char *extension_vsdx="vsdx";
+static const char *extension_xd="xd";
+static const char *extension_xlsx="xlsx";
+static const char *extension_xpi="xpi";
+static const char *extension_xrns="xrns";
+
static const unsigned char zip_header[4] = { 'P', 'K', 0x03, 0x04};
#define ZIP_CENTRAL_DIR 0x02014B50
#define ZIP_FILE_ENTRY 0x04034B50
@@ -84,8 +112,8 @@ struct zip_file_entry {
uint16_t unused1:2; /** Unused */
uint16_t compression; /** Compression method */
- uint16_t last_mod_time; /** Last moditication file time */
- uint16_t last_mod_date; /** Last moditication file date */
+ uint16_t last_mod_time; /** Last modification file time */
+ uint16_t last_mod_date; /** Last modification file date */
uint32_t crc32; /** CRC32 */
uint32_t compressed_size; /** Compressed size */
uint32_t uncompressed_size; /** Uncompressed size */
@@ -106,8 +134,13 @@ struct zip64_extra_entry
typedef struct zip_file_entry zip_file_entry_t;
typedef struct zip64_extra_entry zip64_extra_entry_t;
-static uint32_t expected_compressed_size=0;
+static uint64_t expected_compressed_size=0;
+/*@
+ @ requires \valid(f);
+ @ requires 0 < size <= 4096;
+ @ requires \valid_read((const char *)needle + (0 .. size-1));
+ @*/
static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size)
{
char *buffer =(char *)MALLOC(4096);
@@ -118,30 +151,49 @@ static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size
while (!feof(f))
{
- int count = 0;
- unsigned int left;
- const unsigned int read_size= fread(buffer, 1, 4096, f);
- left = read_size;
-
- while (left>=size)
+ const size_t read_size=fread(buffer, 1, 4096, f);
+ if(read_size <= 0 || total > (0x7fffffffffffffff - 4096))
+ {
+ free(buffer);
+ return -1;
+ }
+ /*@ assert 0 < read_size <= 4096; */
+ /*@ assert total <= 0x8000000000000000 - 4096; */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown(buffer, 4096);
+#endif
+ if(read_size >= size)
{
- if (buffer[count]==*(const char *)needle && memcmp(buffer+count, needle, size)==0)
+ /*@ assert read_size >= size; */
+ const unsigned int count_max=read_size - size;
+ unsigned int count = 0;
+ // TODO loop invariant 0 <= count <= count_max + 1;
+ /*@
+ @ loop variant count_max - count;
+ @*/
+ for(count=0; count <= count_max; count++)
{
- free(buffer);
- if(my_fseek(f, (off_t)count-read_size, SEEK_CUR)<0)
+ /*@ assert count <= count_max; */
+ if (buffer[count]==*(const char *)needle && memcmp(buffer+count, needle, size)==0)
{
- log_trace("zip: file_get_pos count-read failed\n");
- return -1;
+ free(buffer);
+ if(my_fseek(f, (off_t)count-(off_t)read_size, SEEK_CUR)<0)
+ {
+#if !defined(__FRAMAC__)
+ log_trace("zip: file_get_pos count-read failed\n");
+#endif
+ return -1;
+ }
+ return total+count;
}
- return total;
}
- count++;
- total++;
- left--;
+ total+=count_max+1;
}
if(feof(f) || my_fseek(f, (off_t)1-size, SEEK_CUR)<0)
{
+#if !defined(__FRAMAC__)
log_trace("zip: file_get_pos 1-size failed\n");
+#endif
free(buffer);
return -1;
}
@@ -150,6 +202,296 @@ static int64_t file_get_pos(FILE *f, const void* needle, const unsigned int size
return -1;
}
+#ifndef __FRAMAC__
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid(ext);
+ @ requires \valid(krita);
+ @ requires fr->file_size < 0x8000000000000000 - 65535;
+ @ requires 0 < len <= 65535;
+ @ requires *ext == \null ||
+ *ext == extension_apk ||
+ *ext == extension_celtx ||
+ *ext == extension_docx ||
+ *ext == extension_epub ||
+ *ext == extension_jar ||
+ *ext == extension_kmz ||
+ *ext == extension_kra ||
+ *ext == extension_mmap ||
+ *ext == extension_notebook ||
+ *ext == extension_numbers ||
+ *ext == extension_odg ||
+ *ext == extension_odp ||
+ *ext == extension_ods ||
+ *ext == extension_odt ||
+ *ext == extension_ora ||
+ *ext == extension_pages ||
+ *ext == extension_pptx ||
+ *ext == extension_sh3d ||
+ *ext == extension_sketch ||
+ *ext == extension_sxc ||
+ *ext == extension_sxd ||
+ *ext == extension_sxi ||
+ *ext == extension_sxw ||
+ *ext == extension_vsdx ||
+ *ext == extension_xd ||
+ *ext == extension_xlsx ||
+ *ext == extension_xpi ||
+ *ext == extension_xrns ||
+ *ext == file_hint_zip.extension;
+ @ ensures *ext == \null ||
+ *ext == extension_apk ||
+ *ext == extension_celtx ||
+ *ext == extension_docx ||
+ *ext == extension_epub ||
+ *ext == extension_jar ||
+ *ext == extension_kmz ||
+ *ext == extension_kra ||
+ *ext == extension_mmap ||
+ *ext == extension_notebook ||
+ *ext == extension_numbers ||
+ *ext == extension_odg ||
+ *ext == extension_odp ||
+ *ext == extension_ods ||
+ *ext == extension_odt ||
+ *ext == extension_ora ||
+ *ext == extension_pages ||
+ *ext == extension_pptx ||
+ *ext == extension_sh3d ||
+ *ext == extension_sketch ||
+ *ext == extension_sxc ||
+ *ext == extension_sxd ||
+ *ext == extension_sxi ||
+ *ext == extension_sxw ||
+ *ext == extension_vsdx ||
+ *ext == extension_xd ||
+ *ext == extension_xlsx ||
+ *ext == extension_xpi ||
+ *ext == extension_xrns ||
+ *ext == file_hint_zip.extension;
+ @ ensures fr->file_size < 0x8000000000000000;
+ @ ensures \result == -1 || \result == 0;
+ @ ensures *krita==0 || *krita==19;
+ @*/
+static int zip_parse_file_entry_fn(file_recovery_t *fr, const char **ext, const unsigned int file_nbr, const zip_file_entry_t file, const uint64_t len, unsigned int *krita)
+{
+#ifdef __FRAMAC__
+ char *filename=(char *)MALLOC(65535+1);
+#else
+ char *filename=(char *)MALLOC(len+1);
+#endif
+ *krita=0;
+ if (fread(filename, len, 1, fr->handle) != 1)
+ {
+#ifdef DEBUG_ZIP
+ log_trace("zip: Unexpected EOF in file_entry header: %lu bytes expected\n", len);
+#endif
+ free(filename);
+ return -1;
+ }
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown(filename, len);
+#endif
+ fr->file_size += len;
+ /*@ assert fr->file_size < 0x8000000000000000; */
+ filename[len]='\0';
+ if(first_filename[0]=='\0')
+ {
+ const unsigned int len_tmp=(len<255?len:255);
+ strncpy(first_filename, filename, len_tmp);
+ first_filename[len_tmp]='\0';
+ }
+#ifdef DEBUG_ZIP
+ log_info("%s\n", filename);
+#endif
+ if(*ext==NULL)
+ {
+ static int msoffice=0;
+ static int sh3d=0;
+ static const char *ext_msoffice=NULL;
+ if(file_nbr==0)
+ {
+ msoffice=0;
+ sh3d=0;
+ ext_msoffice=NULL;
+ }
+ if(len==19 && memcmp(filename, "[Content_Types].xml", 19)==0)
+ msoffice=1;
+ else if(file_nbr==0)
+ {
+ if(len==8 && memcmp(filename, "mimetype", 8)==0 && le16(file.extra_length)==0)
+ {
+ unsigned char buffer[128];
+ const unsigned int compressed_size=le32(file.compressed_size);
+ const int to_read=(compressed_size < 128 ? compressed_size: 128);
+ if( fread(buffer, to_read, 1, fr->handle)!=1)
+ {
+#ifdef DEBUG_ZIP
+ log_trace("zip: Unexpected EOF in file_entry data: %u bytes expected\n",
+ compressed_size);
+#endif
+ free(filename);
+ return -1;
+ }
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, 128);
+#endif
+ if (my_fseek(fr->handle, -to_read, SEEK_CUR) < 0)
+ {
+ log_info("fseek failed\n");
+ free(filename);
+ return -1;
+ }
+ if(compressed_size==16 && memcmp(buffer,"image/openraster",16)==0)
+ *ext=extension_ora;
+ else if(compressed_size==20 && memcmp(buffer,"application/epub+zip",20)==0)
+ *ext=extension_epub;
+ else if(compressed_size==28 && memcmp(buffer,"application/vnd.sun.xml.calc",28)==0)
+ *ext=extension_sxc;
+ else if(compressed_size==28 && memcmp(buffer,"application/vnd.sun.xml.draw",28)==0)
+ *ext=extension_sxd;
+ else if(compressed_size==31 && memcmp(buffer,"application/vnd.sun.xml.impress",31)==0)
+ *ext=extension_sxi;
+ else if(compressed_size==30 && memcmp(buffer,"application/vnd.sun.xml.writer",30)==0)
+ *ext=extension_sxw;
+ else if(compressed_size==39 && memcmp(buffer,"application/vnd.oasis.opendocument.text",39)==0)
+ *ext=extension_odt;
+ else if(compressed_size==43 && memcmp(buffer,"application/vnd.oasis.opendocument.graphics",43)==0)
+ *ext=extension_odg;
+ else if(compressed_size==46 && memcmp(buffer,"application/vnd.oasis.opendocument.spreadsheet",46)==0)
+ *ext=extension_ods;
+ else if(compressed_size==47 && memcmp(buffer,"application/vnd.oasis.opendocument.presentation",47)==0)
+ *ext=extension_odp;
+ else if(memcmp(buffer,"application/x-krita",19)==0)
+ {
+ *ext=extension_kra;
+ *krita=19;
+ }
+ else
+ { /* default to writer */
+ *ext=extension_sxw;
+ }
+ }
+ /* Zipped Keyhole Markup Language (KML) used by Google Earth */
+ else if(len==7 && memcmp(filename, "doc.kml", 7)==0)
+ *ext=extension_kmz;
+ else if(len==4 && memcmp(filename, "Home", 4)==0)
+ sh3d=1;
+ /* Celtx, Screenwriting & Media Pre-production file */
+ else if(len==9 && memcmp(filename, "local.rdf", 9)==0)
+ *ext=extension_celtx;
+ else if(len==13 && memcmp(filename, "document.json", 13)==0)
+ *ext=extension_sketch;
+ }
+ else if(file_nbr==1 && sh3d==1)
+ {
+ if(len==1 && filename[0]=='0')
+ *ext=extension_sh3d;
+ }
+ if(strncmp(filename, "word/", 5)==0)
+ ext_msoffice=extension_docx;
+ else if(strncmp(filename, "xl/", 3)==0)
+ ext_msoffice=extension_xlsx;
+ else if(strncmp(filename, "ppt/", 4)==0)
+ ext_msoffice=extension_pptx;
+ else if(strncmp(filename, "visio/", 6)==0)
+ ext_msoffice=extension_vsdx;
+ if(msoffice && ext_msoffice!=NULL)
+ *ext=ext_msoffice;
+ }
+ if(*ext==NULL)
+ {
+ /* iWork */
+ if(len==23 && memcmp(filename, "QuickLook/Thumbnail.jpg", 23)==0)
+ *ext=extension_pages;
+ else if(len==20 && strncasecmp(filename, "META-INF/MANIFEST.MF", 20)==0)
+ *ext=extension_jar;
+ else if(len==15 && strncasecmp(filename, "chrome.manifest", 15)==0)
+ *ext=extension_xpi;
+ /* SMART Notebook */
+ else if(len==15 && memcmp(filename, "imsmanifest.xml", 15)==0)
+ *ext=extension_notebook;
+ /* Apple Numbers */
+ else if(len==18 && memcmp(filename, "Index/Document.iwa", 18)==0)
+ *ext=extension_numbers;
+ else if(len==19 && memcmp(filename, "AndroidManifest.xml", 19)==0)
+ *ext=extension_apk;
+ else if(len==30 && memcmp(filename, "xsd/MindManagerApplication.xsd", 30)==0)
+ *ext=extension_mmap;
+ }
+ free(filename);
+ return 0;
+}
+#endif
+
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires \valid(ext);
+ @ requires fr->file_size < 0x8000000000000000 + 4;
+ @ requires \separated(fr, ext);
+ @ requires *ext == \null ||
+ *ext == extension_apk ||
+ *ext == extension_celtx ||
+ *ext == extension_docx ||
+ *ext == extension_epub ||
+ *ext == extension_jar ||
+ *ext == extension_kmz ||
+ *ext == extension_kra ||
+ *ext == extension_mmap ||
+ *ext == extension_notebook ||
+ *ext == extension_numbers ||
+ *ext == extension_odg ||
+ *ext == extension_odp ||
+ *ext == extension_ods ||
+ *ext == extension_odt ||
+ *ext == extension_ora ||
+ *ext == extension_pages ||
+ *ext == extension_pptx ||
+ *ext == extension_sh3d ||
+ *ext == extension_sketch ||
+ *ext == extension_sxc ||
+ *ext == extension_sxd ||
+ *ext == extension_sxi ||
+ *ext == extension_sxw ||
+ *ext == extension_vsdx ||
+ *ext == extension_xd ||
+ *ext == extension_xlsx ||
+ *ext == extension_xpi ||
+ *ext == extension_xrns ||
+ *ext == file_hint_zip.extension;
+ @ ensures *ext == \null ||
+ *ext == extension_apk ||
+ *ext == extension_celtx ||
+ *ext == extension_docx ||
+ *ext == extension_epub ||
+ *ext == extension_jar ||
+ *ext == extension_kmz ||
+ *ext == extension_kra ||
+ *ext == extension_mmap ||
+ *ext == extension_notebook ||
+ *ext == extension_numbers ||
+ *ext == extension_odg ||
+ *ext == extension_odp ||
+ *ext == extension_ods ||
+ *ext == extension_odt ||
+ *ext == extension_ora ||
+ *ext == extension_pages ||
+ *ext == extension_pptx ||
+ *ext == extension_sh3d ||
+ *ext == extension_sketch ||
+ *ext == extension_sxc ||
+ *ext == extension_sxd ||
+ *ext == extension_sxi ||
+ *ext == extension_sxw ||
+ *ext == extension_vsdx ||
+ *ext == extension_xd ||
+ *ext == extension_xlsx ||
+ *ext == extension_xpi ||
+ *ext == extension_xrns ||
+ *ext == file_hint_zip.extension;
+ @*/
static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const unsigned int file_nbr)
{
zip_file_entry_t file;
@@ -163,6 +505,9 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&file, sizeof(file));
+#endif
fr->file_size += sizeof(file);
#ifdef DEBUG_ZIP
log_info("%u Comp=%u %u CRC32=0x%08X extra_length=%u ",
@@ -180,140 +525,22 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
if(fr->time < tmp)
fr->time=tmp;
}
+ if(fr->file_size + 65535 >= 0x8000000000000000)
+ {
+ return -1;
+ }
+ /*@ assert fr->file_size < 0x8000000000000000 - 65535; */
len = le16(file.filename_length);
if (len)
{
- char *filename=(char *)MALLOC(len+1);
- if (fread(filename, len, 1, fr->handle) != 1)
- {
-#ifdef DEBUG_ZIP
- log_trace("zip: Unexpected EOF in file_entry header: %lu bytes expected\n", len);
-#endif
- free(filename);
+ /*@ assert 0 < len <= 65535; */
+#ifndef __FRAMAC__
+ if(zip_parse_file_entry_fn(fr, ext, file_nbr, file, len, &krita) < 0)
return -1;
- }
- fr->file_size += len;
- filename[len]='\0';
- if(first_filename[0]=='\0')
- {
- const unsigned int len_tmp=(len<255?len:255);
- strncpy(first_filename, filename, len_tmp);
- first_filename[len_tmp]='\0';
- }
-#ifdef DEBUG_ZIP
- log_info("%s\n", filename);
#endif
- if(*ext==NULL)
- {
- static int msoffice=0;
- static int sh3d=0;
- static const char *ext_msoffice=NULL;
- if(file_nbr==0)
- {
- msoffice=0;
- sh3d=0;
- ext_msoffice=NULL;
- }
- if(len==19 && memcmp(filename, "[Content_Types].xml", 19)==0)
- msoffice=1;
- else if(file_nbr==0)
- {
- if(len==8 && memcmp(filename, "mimetype", 8)==0 && le16(file.extra_length)==0)
- {
- unsigned char buffer[128];
- const unsigned int compressed_size=le32(file.compressed_size);
- const int to_read=(compressed_size < 128 ? compressed_size: 128);
- if( fread(buffer, to_read, 1, fr->handle)!=1)
- {
-#ifdef DEBUG_ZIP
- log_trace("zip: Unexpected EOF in file_entry data: %u bytes expected\n",
- compressed_size);
-#endif
- free(filename);
- return -1;
- }
- if (my_fseek(fr->handle, -to_read, SEEK_CUR) < 0)
- {
- log_info("fseek failed\n");
- free(filename);
- return -1;
- }
- if(compressed_size==16 && memcmp(buffer,"image/openraster",16)==0)
- *ext="ora";
- else if(compressed_size==20 && memcmp(buffer,"application/epub+zip",20)==0)
- *ext="epub";
- else if(compressed_size==28 && memcmp(buffer,"application/vnd.sun.xml.calc",28)==0)
- *ext="sxc";
- else if(compressed_size==28 && memcmp(buffer,"application/vnd.sun.xml.draw",28)==0)
- *ext="sxd";
- else if(compressed_size==31 && memcmp(buffer,"application/vnd.sun.xml.impress",31)==0)
- *ext="sxi";
- else if(compressed_size==30 && memcmp(buffer,"application/vnd.sun.xml.writer",30)==0)
- *ext="sxw";
- else if(compressed_size==39 && memcmp(buffer,"application/vnd.oasis.opendocument.text",39)==0)
- *ext="odt";
- else if(compressed_size==43 && memcmp(buffer,"application/vnd.oasis.opendocument.graphics",43)==0)
- *ext="odg";
- else if(compressed_size==46 && memcmp(buffer,"application/vnd.oasis.opendocument.spreadsheet",46)==0)
- *ext="ods";
- else if(compressed_size==47 && memcmp(buffer,"application/vnd.oasis.opendocument.presentation",47)==0)
- *ext="odp";
- else if(memcmp(buffer,"application/x-krita",19)==0)
- {
- *ext="kra";
- krita=19;
- }
- else
- { /* default to writer */
- *ext="sxw";
- }
- }
- /* Zipped Keyhole Markup Language (KML) used by Google Earth */
- else if(len==7 && memcmp(filename, "doc.kml", 7)==0)
- *ext="kmz";
- else if(len==4 && memcmp(filename, "Home", 4)==0)
- sh3d=1;
- /* Celtx, Screenwriting & Media Pre-production file */
- else if(len==9 && memcmp(filename, "local.rdf", 9)==0)
- *ext="celtx";
- else if(len==13 && memcmp(filename, "document.json", 13)==0)
- *ext="sketch";
- }
- else if(file_nbr==1 && sh3d==1)
- {
- if(len==1 && filename[0]=='0')
- *ext="sh3d";
- }
- if(strncmp(filename, "word/", 5)==0)
- ext_msoffice="docx";
- else if(strncmp(filename, "xl/", 3)==0)
- ext_msoffice="xlsx";
- else if(strncmp(filename, "ppt/", 4)==0)
- ext_msoffice="pptx";
- else if(strncmp(filename, "visio/", 6)==0)
- ext_msoffice="vsdx";
- if(msoffice && ext_msoffice!=NULL)
- *ext=ext_msoffice;
- }
- if(*ext==NULL)
- {
- /* iWork */
- if(len==23 && memcmp(filename, "QuickLook/Thumbnail.jpg", 23)==0)
- *ext="pages";
- else if(len==20 && strncasecmp(filename, "META-INF/MANIFEST.MF", 20)==0)
- *ext="jar";
- else if(len==15 && strncasecmp(filename, "chrome.manifest", 15)==0)
- *ext="xpi";
- /* SMART Notebook */
- else if(len==15 && memcmp(filename, "imsmanifest.xml", 15)==0)
- *ext="notebook";
- else if(len==19 && memcmp(filename, "AndroidManifest.xml", 19)==0)
- *ext="apk";
- else if(len==30 && memcmp(filename, "xsd/MindManagerApplication.xsd", 30)==0)
- *ext="mmap";
- }
- free(filename);
+ /*@ assert fr->file_size < 0x8000000000000000; */
}
+ /*@ assert fr->file_size < 0x8000000000000000; */
#ifdef DEBUG_ZIP
log_info("\n");
#endif
@@ -321,12 +548,21 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
memset(&extra, 0, sizeof(extra));
if (len>0)
{
+ /*@ assert 0 < len <= 65535; */
+ if(fr->file_size + 65535 >= 0x8000000000000000)
+ {
+ return -1;
+ }
+ /*@ assert fr->file_size < 0x8000000000000000 - 65535; */
if (fread(&extra, sizeof(extra), 1, fr->handle) != 1)
{
#ifdef DEBUG_ZIP
log_trace("zip: Unexpected EOF in file_entry header: %lu bytes expected\n", len);
#endif
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&extra, sizeof(extra));
+#endif
if (my_fseek(fr->handle, fr->file_size, SEEK_SET) == -1 ||
my_fseek(fr->handle, len, SEEK_CUR) == -1)
{
@@ -336,11 +572,15 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
return -1;
}
fr->file_size += len;
+ /*@ assert fr->file_size < 0x8000000000000000; */
}
+ /*@ assert fr->file_size < 0x8000000000000000; */
len = le32(file.compressed_size);
if(len==0xffffffff && le16(extra.tag)==1)
{
len = le64(extra.compressed_size);
+ if(len >= 0x8000000000000000)
+ return -1;
/* Avoid endless loop */
if( fr->file_size + len < fr->file_size)
return -1;
@@ -349,6 +589,10 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
len=krita;
if (len>0)
{
+ /*@ assert len < 0x8000000000000000; */
+ if(fr->file_size + len >= 0x8000000000000000)
+ return -1;
+ /*@ assert fr->file_size + len < 0x8000000000000000; */
if (my_fseek(fr->handle, len, SEEK_CUR) == -1)
{
#ifdef DEBUG_ZIP
@@ -359,8 +603,11 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
#ifdef DEBUG_ZIP
log_trace("zip: Data of length %lu\n", len);
#endif
+ /*@ assert fr->file_size + len < 0x8000000000000000; */
fr->file_size += len;
+ /*@ assert fr->file_size < 0x8000000000000000; */
}
+ /*@ assert fr->file_size < 0x8000000000000000; */
expected_compressed_size=len;
if (file.has_descriptor && (le16(file.compression)==8 || le16(file.compression)==9))
{
@@ -379,13 +626,22 @@ static int zip_parse_file_entry(file_recovery_t *fr, const char **ext, const uns
return -1;
if (pos > 0)
{
+ if(fr->file_size + pos > 0x7fffffffffffffff)
+ return -1;
fr->file_size += pos;
expected_compressed_size=pos;
+ /*@ assert fr->file_size < 0x8000000000000000; */
}
}
+ /*@ assert fr->file_size < 0x8000000000000000; */
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip_parse_central_dir(file_recovery_t *fr)
{
zip_file_entry_t file;
@@ -414,6 +670,9 @@ static int zip_parse_central_dir(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&file, sizeof(file));
+#endif
fr->file_size += sizeof(file);
#ifdef DEBUG_ZIP
log_trace("zip: Central dir with CRC 0x%08X\n", file.crc32);
@@ -426,6 +685,9 @@ static int zip_parse_central_dir(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&dir, sizeof(dir));
+#endif
fr->file_size += sizeof(dir);
/* Rest of the block - could attempt CRC check */
@@ -444,6 +706,12 @@ static int zip_parse_central_dir(file_recovery_t *fr)
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires fr->file_size < 0x8000000000000000;
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip64_parse_end_central_dir(file_recovery_t *fr)
{
struct {
@@ -465,11 +733,16 @@ static int zip64_parse_end_central_dir(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&dir, sizeof(dir));
+#endif
fr->file_size += sizeof(dir);
if (dir.end_size > 0)
{
const uint64_t len = le64(dir.end_size);
+ if(len >= 0x8000000000000000 - sizeof(dir) - 4)
+ return -1;
/* Avoid endless loop */
if( fr->file_size + len <= fr->file_size)
return -1;
@@ -489,6 +762,11 @@ static int zip64_parse_end_central_dir(file_recovery_t *fr)
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip_parse_end_central_dir(file_recovery_t *fr)
{
struct {
@@ -508,6 +786,9 @@ static int zip_parse_end_central_dir(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&dir, sizeof(dir));
+#endif
fr->file_size += sizeof(dir);
if (dir.comment_length)
@@ -528,6 +809,11 @@ static int zip_parse_end_central_dir(file_recovery_t *fr)
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip_parse_data_desc(file_recovery_t *fr)
{
struct {
@@ -543,6 +829,9 @@ static int zip_parse_data_desc(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&desc, sizeof(desc));
+#endif
fr->file_size += sizeof(desc);
#ifdef DEBUG_ZIP
log_info("compressed_size=%u/%u uncompressed_size=%u CRC32=0x%08X\n",
@@ -556,6 +845,11 @@ static int zip_parse_data_desc(file_recovery_t *fr)
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip_parse_signature(file_recovery_t *fr)
{
uint16_t len;
@@ -567,6 +861,9 @@ static int zip_parse_signature(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&len, 2);
+#endif
fr->file_size += 2;
if (len)
@@ -585,6 +882,11 @@ static int zip_parse_signature(file_recovery_t *fr)
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ ensures \result == -1 || \result == 0;
+ @*/
static int zip64_parse_end_central_dir_locator(file_recovery_t *fr)
{
struct {
@@ -600,10 +902,18 @@ static int zip64_parse_end_central_dir_locator(file_recovery_t *fr)
#endif
return -1;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&loc, sizeof(loc));
+#endif
fr->file_size += sizeof(loc);
return 0;
}
+/*@
+ @ requires \valid(fr);
+ @ requires \valid(fr->handle);
+ @ requires fr->file_check==&file_check_zip;
+ @*/
static void file_check_zip(file_recovery_t *fr)
{
const char *ext=NULL;
@@ -611,6 +921,8 @@ static void file_check_zip(file_recovery_t *fr)
fr->file_size = 0;
fr->offset_error=0;
fr->offset_ok=0;
+ /* fr->time is already set to 0 but it helps frama-c */
+ fr->time=0;
first_filename[0]='\0';
if(my_fseek(fr->handle, 0, SEEK_SET) < 0)
return ;
@@ -619,7 +931,13 @@ static void file_check_zip(file_recovery_t *fr)
uint64_t file_size_old;
uint32_t header;
int status;
-
+ if(file_nbr>=0xffffffff || fr->file_size >= 0x8000000000000000 - 4)
+ {
+ fr->offset_error = fr->file_size;
+ fr->file_size = 0;
+ return;
+ }
+ /*@ assert fr->file_size < 0x8000000000000000 - 4; */
if (fread(&header, 4, 1, fr->handle)!=1)
{
#ifdef DEBUG_ZIP
@@ -629,7 +947,9 @@ static void file_check_zip(file_recovery_t *fr)
fr->file_size=0;
return;
}
-
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&header, 4);
+#endif
header = le32(header);
#ifdef DEBUG_ZIP
log_trace("Header 0x%08X at 0x%llx\n", header, (long long unsigned int)fr->file_size);
@@ -637,6 +957,7 @@ static void file_check_zip(file_recovery_t *fr)
#endif
fr->file_size += 4;
file_size_old=fr->file_size;
+ /*@ assert fr->file_size < 0x8000000000000000; */
switch (header)
{
@@ -687,26 +1008,45 @@ static void file_check_zip(file_recovery_t *fr)
}
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_zip;
+ @*/
+/* TODO ensures valid_read_string((char*)file_recovery->filename); */
static void file_rename_zip(file_recovery_t *file_recovery)
{
const char *ext=NULL;
unsigned int file_nbr=0;
file_recovery_t fr;
reset_file_recovery(&fr);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
if((fr.handle=fopen(file_recovery->filename, "rb"))==NULL)
+ {
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
+ }
fr.file_size = 0;
fr.offset_error=0;
first_filename[0]='\0';
if(my_fseek(fr.handle, 0, SEEK_SET) < 0)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
+ /*@ loop invariant valid_read_string((char*)file_recovery->filename); */
while (1)
{
uint32_t header;
int status;
+ if(file_nbr>=0xffffffff || fr.file_size >= 0x8000000000000000 - 4)
+ {
+ fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
+ return;
+ }
+ /*@ assert fr.file_size < 0x8000000000000000 - 4; */
if (fread(&header, 4, 1, fr.handle)!=1)
{
@@ -714,8 +1054,12 @@ static void file_rename_zip(file_recovery_t *file_recovery)
log_trace("Failed to read block header\n");
#endif
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)&header, 4);
+#endif
header = le32(header);
#ifdef DEBUG_ZIP
@@ -747,7 +1091,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if(ext!=NULL)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, NULL, 0, 0, ext, 1);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
break;
@@ -769,6 +1115,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if (status<0)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
/* Only end of central dir is end of archive, 64b version of it is before */
@@ -782,12 +1129,56 @@ static void file_rename_zip(file_recovery_t *file_recovery)
first_filename[len]!='/' &&
first_filename[len]!='\\';
len++);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, first_filename, len, 0, "zip", 0);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
}
}
+/*@
+ @ requires buffer_size >= 85;
+ @ 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->extension);
+ @ requires file_recovery->file_stat==\null || valid_read_string((char*)file_recovery->filename);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ requires separation: \separated(&file_hint_zip, file_recovery, file_recovery_new);
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->file_stat == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->handle == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->time == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 30);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_zip || file_recovery_new->file_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_zip || file_recovery_new->file_rename == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_zip.extension ||
+ file_recovery_new->extension == extension_docx ||
+ file_recovery_new->extension == extension_epub ||
+ file_recovery_new->extension == extension_kra ||
+ file_recovery_new->extension == extension_numbers ||
+ file_recovery_new->extension == extension_odg ||
+ file_recovery_new->extension == extension_odp ||
+ file_recovery_new->extension == extension_ods ||
+ file_recovery_new->extension == extension_odt ||
+ file_recovery_new->extension == extension_ora ||
+ file_recovery_new->extension == extension_pptx ||
+ file_recovery_new->extension == extension_sh3d ||
+ file_recovery_new->extension == extension_sxc ||
+ file_recovery_new->extension == extension_sxd ||
+ file_recovery_new->extension == extension_sxi ||
+ file_recovery_new->extension == extension_sxw ||
+ file_recovery_new->extension == extension_vsdx ||
+ file_recovery_new->extension == extension_xd ||
+ file_recovery_new->extension == extension_xlsx ||
+ file_recovery_new->extension == extension_xrns );
+ @ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
+ @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
static int header_check_zip(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 zip_file_entry_t *file=(const zip_file_entry_t *)&buffer[4];
@@ -795,12 +1186,18 @@ static int header_check_zip(const unsigned char *buffer, const unsigned int buff
#ifdef DEBUG_ZIP
log_trace("header_check_zip\n");
#endif
+ if(len==0 || len > 4096)
+ return 0;
+ if(le16(file->version) < 10)
+ return 0;
+#ifndef MAIN_zip
if(file_recovery->file_stat!=NULL &&
file_recovery->file_stat->file_hint==&file_hint_doc)
{
if(header_ignored_adv(file_recovery, file_recovery_new)==0)
return 0;
}
+#endif
/* A zip file begins by ZIP_FILE_ENTRY, this signature can also be
* found for each compressed file */
if(file_recovery->file_stat!=NULL &&
@@ -811,63 +1208,63 @@ static int header_check_zip(const unsigned char *buffer, const unsigned int buff
return 0;
}
reset_file_recovery(file_recovery_new);
- file_recovery_new->min_filesize=21;
+ file_recovery_new->min_filesize=30; /* 4+sizeof(file) == 30 */
file_recovery_new->file_check=&file_check_zip;
if(len==8 && memcmp(&buffer[30],"mimetype",8)==0)
{
const unsigned int compressed_size=le32(file->compressed_size);
/* Mypaint .ora */
if(compressed_size==16 && memcmp(&buffer[38],"image/openraster",16)==0)
- file_recovery_new->extension="ora";
+ file_recovery_new->extension=extension_ora;
else if(compressed_size==20 && memcmp(&buffer[38],"application/epub+zip",20)==0)
- file_recovery_new->extension="epub";
+ file_recovery_new->extension=extension_epub;
else if(compressed_size==28 && memcmp(&buffer[38],"application/vnd.sun.xml.calc",28)==0)
- file_recovery_new->extension="sxc";
+ file_recovery_new->extension=extension_sxc;
else if(compressed_size==28 && memcmp(&buffer[38],"application/vnd.sun.xml.draw",28)==0)
- file_recovery_new->extension="sxd";
+ file_recovery_new->extension=extension_sxd;
else if(compressed_size==31 && memcmp(&buffer[38],"application/vnd.sun.xml.impress",31)==0)
- file_recovery_new->extension="sxi";
+ file_recovery_new->extension=extension_sxi;
else if(compressed_size==30 && memcmp(&buffer[38],"application/vnd.sun.xml.writer",30)==0)
- file_recovery_new->extension="sxw";
+ file_recovery_new->extension=extension_sxw;
else if(compressed_size==39 && memcmp(&buffer[38],"application/vnd.oasis.opendocument.text",39)==0)
- file_recovery_new->extension="odt";
+ file_recovery_new->extension=extension_odt;
else if(compressed_size==43 && memcmp(&buffer[38],"application/vnd.oasis.opendocument.graphics",43)==0)
- file_recovery_new->extension="odg";
+ file_recovery_new->extension=extension_odg;
else if(compressed_size==45 && memcmp(&buffer[38],"application/vnd.adobe.sparkler.project+dcxucf",45)==0)
- file_recovery_new->extension="xd";
+ file_recovery_new->extension=extension_xd;
else if(compressed_size==46 && memcmp(&buffer[38],"application/vnd.oasis.opendocument.spreadsheet",46)==0)
- file_recovery_new->extension="ods";
+ file_recovery_new->extension=extension_ods;
else if(compressed_size==47 && memcmp(&buffer[38],"application/vnd.oasis.opendocument.presentation",47)==0)
- file_recovery_new->extension="odp";
+ file_recovery_new->extension=extension_odp;
else if(memcmp(&buffer[38],"application/x-krita",19)==0)
- file_recovery_new->extension="kra";
+ file_recovery_new->extension=extension_kra;
else
{ /* default to writer */
- file_recovery_new->extension="sxw";
+ file_recovery_new->extension=extension_sxw;
}
}
else if(len==19 && memcmp(&buffer[30],"[Content_Types].xml",19)==0)
{
if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"word/", 5)!=0)
- file_recovery_new->extension="docx";
+ file_recovery_new->extension=extension_docx;
else if(pos_in_mem(&buffer[0], 2000, (const unsigned char*)"xl/", 3)!=0)
- file_recovery_new->extension="xlsx";
+ file_recovery_new->extension=extension_xlsx;
else if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"ppt/", 4)!=0)
- file_recovery_new->extension="pptx";
+ file_recovery_new->extension=extension_pptx;
else if(pos_in_mem(&buffer[0], buffer_size, (const unsigned char*)"visio/", 6)!=0)
- file_recovery_new->extension="vsdx";
+ file_recovery_new->extension=extension_vsdx;
else
- file_recovery_new->extension="docx";
+ file_recovery_new->extension=extension_docx;
file_recovery_new->file_rename=&file_rename_zip;
}
/* Extended Renoise song file */
else if(len==8 && memcmp(&buffer[30], "Song.xml", 8)==0)
- file_recovery_new->extension="xrns";
+ file_recovery_new->extension=extension_xrns;
else if(len==4 && memcmp(&buffer[30], "Home", 4)==0)
- file_recovery_new->extension="sh3d";
+ file_recovery_new->extension=extension_sh3d;
/* Apple Numbers */
else if(len==18 && memcmp(&buffer[30], "Index/Document.iwa", 18)==0)
- file_recovery_new->extension="numbers";
+ file_recovery_new->extension=extension_numbers;
else
{
file_recovery_new->extension=file_hint_zip.extension;
@@ -876,6 +1273,18 @@ static int header_check_zip(const unsigned char *buffer, const unsigned int buff
return 1;
}
+/*@
+ @ requires buffer_size >= 85;
+ @ 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;
+ @ requires separation: \separated(&file_hint_zip, file_recovery, file_recovery_new);
+ @ ensures \result == 1;
+ @ ensures file_recovery_new->file_check == &file_check_zip;
+ @ ensures file_recovery_new->extension == file_hint_zip.extension;
+ @*/
static int header_check_winzip(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)
{
reset_file_recovery(file_recovery_new);
@@ -884,20 +1293,136 @@ static int header_check_winzip(const unsigned char *buffer, const unsigned int b
return 1;
}
+/*@
+ @ requires haystack_size > 0;
+ @ requires needle_size > 0;
+ @ requires \valid_read(haystack + (0 .. haystack_size-1));
+ @ requires \valid_read(needle + (0 .. needle_size-1));
+ @ assigns \nothing;
+ @ ensures \result <= haystack_size;
+ @*/
static unsigned int pos_in_mem(const unsigned char *haystack, const unsigned int haystack_size, const unsigned char *needle, const unsigned int needle_size)
{
unsigned int i;
if(haystack_size < needle_size)
return 0;
+ /*@
+ @ loop invariant 0 <= i <= haystack_size - needle_size + 1;
+ @ loop assigns i;
+ @ loop variant haystack_size - needle_size - i;
+ @*/
for(i=0; i <= haystack_size - needle_size; i++)
if(memcmp(&haystack[i],needle,needle_size)==0)
return (i+needle_size);
return 0;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_zip(file_stat_t *file_stat)
{
static const unsigned char zip_header2[8] = { 'P', 'K', '0', '0', 'P', 'K', 0x03, 0x04}; /* WinZIPv8-compressed files. */
register_header_check(0, zip_header,sizeof(zip_header), &header_check_zip, file_stat);
register_header_check(0, zip_header2,sizeof(zip_header2), &header_check_winzip, file_stat);
}
+
+#if defined(MAIN_zip)
+#define BLOCKSIZE 65536u
+int main()
+{
+ const char fn[] = "recup_dir.1/f0000000.zip";
+ unsigned char buffer[BLOCKSIZE];
+ 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);
+ /*@ assert file_recovery.file_stat == \null; */
+ 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_zip;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ register_header_check_zip(&file_stats);
+ if(header_check_zip(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.min_filesize == 30; */
+ /*@ assert file_recovery_new.file_check == &file_check_zip || file_recovery_new.file_check == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
+ /*@ assert file_recovery_new.time == 0; */
+ {
+ 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 */
+ /*@ assert file_recovery_new.extension == file_hint_zip.extension ||
+ file_recovery_new.extension == extension_docx ||
+ file_recovery_new.extension == extension_epub ||
+ file_recovery_new.extension == extension_kra ||
+ file_recovery_new.extension == extension_numbers ||
+ file_recovery_new.extension == extension_odg ||
+ file_recovery_new.extension == extension_odp ||
+ file_recovery_new.extension == extension_ods ||
+ file_recovery_new.extension == extension_odt ||
+ file_recovery_new.extension == extension_ora ||
+ file_recovery_new.extension == extension_pptx ||
+ file_recovery_new.extension == extension_sh3d ||
+ file_recovery_new.extension == extension_sxc ||
+ file_recovery_new.extension == extension_sxd ||
+ file_recovery_new.extension == extension_sxi ||
+ file_recovery_new.extension == extension_sxw ||
+ file_recovery_new.extension == extension_vsdx ||
+ file_recovery_new.extension == extension_xd ||
+ file_recovery_new.extension == extension_xlsx ||
+ file_recovery_new.extension == extension_xrns; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ header_check_zip(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.time == 0; */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL && file_recovery_new.file_check !=NULL)
+ {
+ /*@ assert file_recovery_new.file_check == &file_check_zip; */
+ /*@ assert file_recovery_new.time == 0; */
+ file_check_zip(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ if(file_recovery_new.file_rename!=NULL)
+ {
+ /*@ assert file_recovery_new.file_rename == &file_rename_zip; */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_rename_zip(&file_recovery_new);
+ }
+ return 0;
+}
+#endif