summaryrefslogtreecommitdiffstats
path: root/src/file_txt.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/file_txt.c')
-rw-r--r--src/file_txt.c3803
1 files changed, 3200 insertions, 603 deletions
diff --git a/src/file_txt.c b/src/file_txt.c
index 289beb7..52484d8 100644
--- a/src/file_txt.c
+++ b/src/file_txt.c
@@ -33,6 +33,7 @@
#include <time.h>
#endif
#include <ctype.h> /* tolower */
+#include <assert.h>
#include <stdio.h>
#include "types.h"
#include "common.h"
@@ -40,41 +41,109 @@
#include "log.h"
#include "memmem.h"
#include "file_txt.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
+#if !defined(MAIN_txt)
extern const file_hint_t file_hint_doc;
extern const file_hint_t file_hint_jpg;
extern const file_hint_t file_hint_pdf;
extern const file_hint_t file_hint_sld;
extern const file_hint_t file_hint_tiff;
extern const file_hint_t file_hint_zip;
+#endif
-static inline int filtre(unsigned int car);
+typedef struct
+{
+ const char *string;
+ const unsigned int len;
+ const char *extension;
+} txt_header_t;
-static void register_header_check_txt(file_stat_t *file_stat);
-static int header_check_txt(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 register_header_check_fasttxt(file_stat_t *file_stat);
static void register_header_check_snz(file_stat_t *file_stat);
-static int header_check_fasttxt(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 register_header_check_txt(file_stat_t *file_stat);
+
+static const char *extension_asp="asp";
+static const char *extension_bat="bat";
+static const char *extension_c="c";
+static const char *extension_csv="csv";
+static const char *extension_dc="dc";
+static const char *extension_emlx="emlx";
+static const char *extension_ers="ers";
+static const char *extension_f="f";
+static const char *extension_fb2="fb2";
+static const char *extension_fods="fods";
+static const char *extension_fst="fst";
+static const char *extension_gcs="gcs";
+static const char *extension_ghx="ghx";
+static const char *extension_go="go";
+static const char *extension_gpx="gpx";
+static const char *extension_groovy="groovy";
+static const char *extension_gsb="gsb";
+static const char *extension_h="h";
+#ifdef DJGPP
+static const char *extension_html="htm";
+#else
+static const char *extension_html="html";
+#endif
+static const char *extension_ics="ics";
+static const char *extension_inf="inf";
+static const char *extension_ini="ini";
+#ifdef DJGPP
+static const char *extension_java="jav";
+#else
+static const char *extension_java="java";
+#endif
+static const char *extension_json="json";
+static const char *extension_jsp="jsp";
+static const char *extension_ldif="ldif";
+static const char *extension_ly="ly";
+static const char *extension_mbox="mbox";
+static const char *extension_php="php";
+static const char *extension_pl="pl";
+#ifdef DJGPP
+static const char *extension_plist="pli";
+#else
+static const char *extension_plist="plist";
+#endif
+static const char *extension_pm="pm";
+static const char *extension_prproj="prproj";
+static const char *extension_py="py";
+static const char *extension_rb="rb";
+static const char *extension_rtf="rtf";
+static const char *extension_sla="sla";
+static const char *extension_smil="smil";
+static const char *extension_stl="stl";
+static const char *extension_svg="svg";
+static const char *extension_ttd="ttd";
+static const char *extension_tex="tex";
#ifdef UTF16
-static int header_check_le16_txt(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 const char *extension_utf16="utf16";
#endif
+static const char *extension_vb="vb";
+static const char *extension_vbm="vbm";
+static const char *extension_vcf="vcf";
+static const char *extension_xml="xml";
+static const char *extension_xmp="xmp";
-const file_hint_t file_hint_snz= {
- .extension="snz",
- .description="Olfaction SeeNez odorama",
+const file_hint_t file_hint_fasttxt= {
+ .extension="tx?",
+ .description="Text files with header: rtf,xml,xhtml,mbox/imm,pm,ram,reg,sh,slk,stp,jad,url",
.max_filesize=PHOTOREC_MAX_FILE_SIZE,
.recover=1,
.enable_by_default=1,
- .register_header_check=&register_header_check_snz
+ .register_header_check=&register_header_check_fasttxt
};
-const file_hint_t file_hint_fasttxt= {
- .extension="tx?",
- .description="Text files with header: rtf,xml,xhtml,mbox/imm,pm,ram,reg,sh,slk,stp,jad,url",
+const file_hint_t file_hint_snz= {
+ .extension="snz",
+ .description="Olfaction SeeNez odorama",
.max_filesize=PHOTOREC_MAX_FILE_SIZE,
.recover=1,
.enable_by_default=1,
- .register_header_check=&register_header_check_fasttxt
+ .register_header_check=&register_header_check_snz
};
const file_hint_t file_hint_txt= {
@@ -88,28 +157,6 @@ const file_hint_t file_hint_txt= {
static unsigned char ascii_char[256];
-static void register_header_check_txt(file_stat_t *file_stat)
-{
- unsigned int i;
- for(i=0; i<256; i++)
- ascii_char[i]=i;
- for(i=0; i<256; i++)
- {
- if(filtre(i) || i==0xE2 || i==0xC2 || i==0xC3 || i==0xC5 || i==0xC6 || i==0xCB)
- register_header_check(0, &ascii_char[i], 1, &header_check_txt, file_stat);
- }
-#ifdef UTF16
- register_header_check(1, &ascii_char[0], 1, &header_check_le16_txt, file_stat);
-#endif
-}
-
-typedef struct
-{
- const char *string;
- const unsigned int len;
- const char *extension;
-} txt_header_t;
-
static const txt_header_t fasttxt_headers[] = {
/* Unix shell */
{ "#!/bin/bash", 11, "sh"},
@@ -118,6 +165,11 @@ static const txt_header_t fasttxt_headers[] = {
{ "#! /bin/bash", 12, "sh"},
{ "#! /bin/ksh", 11, "sh"},
{ "#! /bin/sh", 10, "sh"},
+ { "#!/usr/bin/env groovy", 21, "groovy"},
+ { "#!/usr/bin/env perl", 19, "pl"},
+ { "#!/usr/bin/env php", 18, "php"},
+ { "#!/usr/bin/env python", 21, "py"},
+ { "#!/usr/bin/env ruby", 19, "rb"},
/* Opera Hotlist bookmark/contact list/notes */
{ "Opera Hotlist version 2.0", 25, "adr"},
/* Microsoft VB Class module */
@@ -166,6 +218,7 @@ static const txt_header_t fasttxt_headers[] = {
{ "-- phpMyAdmin SQL Dump", 22, "sql"},
{ "--\n-- PostgreSQL database cluster dump", 38, "sql"},
{ "--\r\n-- PostgreSQL database cluster dump", 39, "sql"},
+ { "# ************************************************************\n# Sequel Pro SQL dump", 84, "sql"},
{ "---- BEGIN SSH2 PUBLIC KEY ----", 31, "ppk"},
{ "PuTTY-User-Key-File-2:", 22, "ppk"},
{ "-----BEGIN PGP PRIVATE KEY BLOCK-----", 37, "priv"},
@@ -221,6 +274,9 @@ static const txt_header_t fasttxt_headers[] = {
// #define DEBUG_FILETXT
/* return 1 if char can be found in text file */
+/*@
+ @ assigns \nothing;
+ @*/
static int filtre(unsigned int car)
{
switch(car)
@@ -281,16 +337,192 @@ static int filtre(unsigned int car)
return 0;
}
+/*@
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ assigns \nothing;
+ @*/
+static int has_newline(const char *buffer, const unsigned int buffer_size)
+{
+ unsigned int i;
+ /*@
+ @ loop invariant 0 <= i <= 512;
+ @ loop assigns i;
+ @ loop variant 512-i;
+ @*/
+ for(i=0; i<512 && i < buffer_size && buffer[i]!='\0'; i++)
+ {
+ if(buffer[i]=='\n')
+ return 1;
+ }
+ /* A text file must contains several lines */
+ return 0;
+}
+
+/*@
+ @ requires buffer_size > 0;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ assigns \nothing;
+ @*/
+static unsigned int is_csv(const char *buffer, const unsigned int buffer_size)
+{
+ unsigned int csv_per_line_current=0;
+ unsigned int csv_per_line=0;
+ unsigned int line_nbr=0;
+ unsigned int i;
+ /*@
+ @ loop invariant 0 <= i <= buffer_size;
+ @ loop invariant csv_per_line_current <= i+1;
+ @ loop invariant line_nbr <= i+1;
+ @ loop assigns i, csv_per_line_current, csv_per_line, line_nbr;
+ @ loop variant buffer_size-i;
+ @*/
+ for(i=0; i<buffer_size; i++)
+ {
+ if(buffer[i]==';')
+ {
+ csv_per_line_current++;
+ }
+ else if(buffer[i]=='\n')
+ {
+ if(line_nbr==0)
+ {
+ if(csv_per_line_current==0)
+ return 0;
+ csv_per_line=csv_per_line_current;
+ }
+ if(csv_per_line_current!=csv_per_line)
+ return 0;
+ line_nbr++;
+ csv_per_line_current=0;
+ }
+ }
+ if(line_nbr<10)
+ return 0;
+ return 1;
+}
+
+/*@
+ @ requires valid_read_string(buffer);
+ @ assigns \nothing;
+ @*/
+static unsigned int is_fortran(const char *buffer)
+{
+ const char *str=buffer;
+ unsigned int i=0;
+ /* Detect Fortran */
+ /*@ assert valid_read_string(str); */
+ /*@
+ @ loop invariant 0 <= i <= 10;
+ @ loop assigns str,i;
+ @ loop variant 10 - i;
+ @*/
+ for(i=0; i<10; i++)
+ {
+ str=strstr(str, "\n ");
+ if(str==NULL)
+ return 0;
+ /*@ assert valid_read_string(str); */
+#ifdef __FRAMAC__
+ if(*str=='\0')
+ return 0;
+#endif
+ str++;
+ /*@ assert valid_read_string(str); */
+ }
+ if(i < 10)
+ return 0;
+ if(strstr(buffer, "integer")==NULL)
+ return 0;
+ return 1;
+}
+
+/*@
+ @ requires valid_read_string((char *)buffer);
+ @ assigns \nothing;
+ @*/
+static int is_ini(const unsigned char *buffer)
+{
+ const unsigned char *src=buffer;
+ if(*src!='[')
+ return 0;
+ src++;
+ /*@
+ @ loop assigns src;
+ @*/
+ while(*src!='\0')
+ {
+ if(*src==']')
+ {
+ if(src > buffer + 3)
+ return 1;
+ return 0;
+ }
+ if(!isalnum(*src) && *src!=' ')
+ return 0;
+ src++;
+ }
+ return 0;
+}
+
+/*@
+ @ requires buffer_size >= 0;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @*/
+static double is_random(const unsigned char *buffer, const unsigned int buffer_size)
+{
+ unsigned int stats[256];
+ unsigned int i;
+ double ind;
+ if(buffer_size < 2)
+ return 1;
+ memset(&stats, 0, sizeof(stats));
+ /*@ assert \forall int j; (0 <= j <= 255) ==> (stats[j] == 0); */
+#ifndef __FRAMAC__
+ /*@
+ @ loop invariant 0 <= i <= buffer_size;
+ @ loop invariant \forall integer j; (0 <= j <= 255) ==> (stats[j] <= i+1);
+ @ loop assigns i, stats[0..255];
+ @ loop variant buffer_size-i;
+ @*/
+ for(i=0; i<buffer_size; i++)
+ stats[buffer[i]]++;
+ ind=0;
+ /*@
+ @ loop invariant 0 <= i <= 256;
+ @ loop assigns ind;
+ @ loop variant 256-i;
+ @*/
+ for(i=0; i<256; i++)
+ if(stats[i]>0)
+ ind+=stats[i]*(stats[i]-1);
+#else
+ ind=Frama_C_interval(0, buffer_size*(buffer_size-1));
+#endif
+return ind/buffer_size/(buffer_size-1);
+}
+
/* destination should have an extra byte available for null terminator
- return read size */
-int UTF2Lat(unsigned char *buffer_lower, const unsigned char *buffer, const int buf_len)
+ return written size */
+/*@
+ @ requires buf_len > 0;
+ @ requires \valid(buffer_lower + (0..buf_len-1));
+ @ requires \valid_read(buffer + (0..buf_len-1));
+ @ ensures \result <= buf_len;
+ @*/
+static int UTF2Lat(unsigned char *buffer_lower, const unsigned char *buffer, const int buf_len)
{
const unsigned char *p; /* pointers to actual position in source buffer */
unsigned char *q; /* pointers to actual position in destination buffer */
- int i; /* counter of remaining bytes available in destination buffer */
- for (i = buf_len, p = buffer, q = buffer_lower; p-buffer<buf_len && i > 0 && *p!='\0';)
+ unsigned int offset_dst;
+ /* destination will be null terminated */
+ /*@
+ @ loop invariant offset_dst < buf_len;
+ @ loop invariant q == buffer_lower + offset_dst;
+ @ loop variant buf_len - 1 - offset_dst;
+ @*/
+ for (offset_dst = 0, p = buffer, q = buffer_lower;
+ p+2-buffer<buf_len && offset_dst < buf_len-1 && *p!='\0';)
{
- const unsigned char *p_org=p;
if((*p & 0xf0)==0xe0 && (*(p+1) & 0xc0)==0x80 && (*(p+2) & 0xc0)==0x80)
{ /* UTF8 l=3 */
#ifdef DEBUG_TXT
@@ -384,12 +616,17 @@ int UTF2Lat(unsigned char *buffer_lower, const unsigned char *buffer, const int
}
p+=2;
}
+ else if( 'A' <= *p && *p <='Z')
+ {
+ *q = *p-'A'+'a';
+ p++;
+ }
else
{ /* Ascii UCS */
#ifdef DEBUG_TXT
log_info("UTF8 Ascii UCS 0x%02x\n", *p);
#endif
- *q = tolower(*p);
+ *q = *p;
p++;
}
if (*q=='\0' || filtre(*q)==0)
@@ -398,19 +635,25 @@ int UTF2Lat(unsigned char *buffer_lower, const unsigned char *buffer, const int
log_warning("UTF2Lat reject 0x%x\n",*q);
#endif
*q = '\0';
- return(p_org-buffer);
+ return offset_dst;
}
q++;
- i--;
+ offset_dst++;
}
*q = '\0';
- return(p-buffer);
+ return offset_dst;
}
-static int UTFsize(const unsigned char *buffer, const unsigned int buf_len)
+int UTFsize(const unsigned char *buffer, const unsigned int buf_len)
{
const unsigned char *p=buffer; /* pointers to actual position in source buffer */
unsigned int i=0;
+ /*@
+ @ loop invariant 0 <= i < buf_len + 3;
+ @ loop invariant p == buffer + i;
+ @ loop assigns i, p;
+ @ loop variant buf_len - 1 - i;
+ @*/
while(i<buf_len && *p!='\0')
{
/* Reject some invalid UTF-8 sequences */
@@ -475,47 +718,68 @@ static int UTFsize(const unsigned char *buffer, const unsigned int buf_len)
return (i<buf_len?i:buf_len);
}
+/*@
+ @ requires buffer_size >= 2 && (buffer_size&1)==0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_html;
+ @ assigns file_recovery->calculated_file_size;
+ @ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @*/
static data_check_t data_check_html(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
const char sign_html_end[] = "</html>";
- const unsigned int i=UTFsize(&buffer[buffer_size/2], buffer_size/2);
- unsigned int j;
- for(j=(buffer_size/2>sizeof(sign_html_end)?buffer_size/2-sizeof(sign_html_end):0);
- j+sizeof(sign_html_end)-1 < buffer_size;
- j++)
+ if(buffer_size/2 > (sizeof(sign_html_end)-1))
{
- if(buffer[j]=='<' && strncasecmp((const char *)&buffer[j], sign_html_end, sizeof(sign_html_end)-1)==0)
+ unsigned int j;
+ /*@
+ @ loop assigns j, file_recovery->calculated_file_size;
+ @*/
+ for(j=buffer_size/2-(sizeof(sign_html_end)-1);
+ j+sizeof(sign_html_end)-1 < buffer_size;
+ j++)
{
- file_recovery->calculated_file_size+=j-buffer_size/2+sizeof(sign_html_end)-1;
- return DC_STOP;
+ if(buffer[j]=='<' && strncasecmp((const char *)&buffer[j], sign_html_end, sizeof(sign_html_end)-1)==0)
+ {
+ j+=sizeof(sign_html_end)-1;
+ /*@ assert j >= buffer_size/2; */
+ /*@ loop assigns j; */
+ while(j < buffer_size && (buffer[j]=='\n' || buffer[j]=='\r'))
+ j++;
+ file_recovery->calculated_file_size+=j-buffer_size/2;
+ return DC_STOP;
+ }
}
}
- if(i<buffer_size/2)
{
- if(i>=10)
- file_recovery->calculated_file_size=file_recovery->file_size+i;
- return DC_STOP;
- }
- file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
- return DC_CONTINUE;
-}
-
-static data_check_t data_check_txt(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
-{
- const unsigned int i=UTFsize(&buffer[buffer_size/2], buffer_size/2);
- if(i<buffer_size/2)
- {
- if(i>=10)
- file_recovery->calculated_file_size=file_recovery->file_size+i;
- return DC_STOP;
+ const unsigned int i=UTFsize(&buffer[buffer_size/2], buffer_size/2);
+ if(i<buffer_size/2)
+ {
+ if(i>=10)
+ file_recovery->calculated_file_size=file_recovery->file_size+i;
+ return DC_STOP;
+ }
}
file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
return DC_CONTINUE;
}
+/*@
+ @ requires buffer_size >= 2 && (buffer_size&1)==0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_ttd;
+ @ assigns file_recovery->calculated_file_size;
+ @ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @*/
static data_check_t data_check_ttd(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
unsigned int i;
+ /*@
+ @ loop invariant buffer_size/2 <= i <= buffer_size;
+ @ loop assigns i, file_recovery->calculated_file_size;
+ @ loop variant buffer_size - i;
+ @*/
for(i=buffer_size/2; i<buffer_size; i++)
{
const unsigned char car=buffer[i];
@@ -528,159 +792,139 @@ static data_check_t data_check_ttd(const unsigned char *buffer, const unsigned i
return DC_CONTINUE;
}
-static int header_check_ttd(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)
-{
- if(buffer[56]<'0' || buffer[56]>'9')
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_ttd;
- file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="ttd";
- return 1;
-}
-
-static void file_check_ers(file_recovery_t *file_recovery)
-{
- file_search_footer(file_recovery, "DatasetHeader End", 17, 0);
- file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
-}
-
-static int header_check_ers(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)
-{
- /* ER Mapper Rasters (ERS) */
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_ers;
- file_recovery_new->extension="ers";
- return 1;
-}
-
-static int header_check_ics(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size >= 2 && (buffer_size&1)==0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_txt;
+ @ assigns file_recovery->calculated_file_size;
+ @ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @*/
+static data_check_t data_check_txt(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
- const char *date_asc;
- char *buffer2;
- if(buffer[15]=='\0')
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_size;
- /* vcalendar */
- file_recovery_new->extension="ics";
- /* DTSTART:19970714T133000 ;Local time
- * DTSTART:19970714T173000Z ;UTC time
- * DTSTART;TZID=US-Eastern:19970714T133000 ;Local time and time
- */
- buffer2=(char *)MALLOC(buffer_size+1);
- buffer2[buffer_size]='\0';
- memcpy(buffer2, buffer, buffer_size);
- date_asc=strstr(buffer2, "DTSTART");
- if(date_asc!=NULL)
- date_asc=strchr(date_asc, ':');
- if(date_asc!=NULL && date_asc+1+14 < buffer2+buffer_size)
+ const unsigned int i=UTFsize(&buffer[buffer_size/2], buffer_size/2);
+ if(i<buffer_size/2)
{
- file_recovery_new->time=get_time_from_YYYYMMDD_HHMMSS(date_asc+1);
+ if(i>=10)
+ file_recovery->calculated_file_size=file_recovery->file_size+i;
+ return DC_STOP;
}
- free(buffer2);
- return 1;
+ file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
+ return DC_CONTINUE;
}
-static int header_check_perlm(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size >= 10 && (buffer_size&1)==0;
+ @ requires \valid_read((char *)buffer+(0..buffer_size-1));
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_xml_utf8;
+ @ assigns file_recovery->calculated_file_size,file_recovery->data_check;
+ @ ensures \result == DC_STOP || \result == DC_CONTINUE;
+ @ ensures \result == DC_CONTINUE ==> (file_recovery->data_check==&data_check_txt);
+ @*/
+static data_check_t data_check_xml_utf8(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
unsigned int i;
- const unsigned int buffer_size_test=(buffer_size < 2048 ? buffer_size : 2048);
- for(i=0; i<128 && buffer[i]!=';' && buffer[i]!='\n'; i++);
- if(buffer[i]!=';')
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_size;
- if( td_memmem(buffer, buffer_size_test, "class", 5)!=NULL ||
- td_memmem(buffer, buffer_size_test, "private static", 14)!=NULL ||
- td_memmem(buffer, buffer_size_test, "public interface", 16)!=NULL)
- {
- /* source code in java */
-#ifdef DJGPP
- file_recovery_new->extension="jav";
-#else
- file_recovery_new->extension="java";
-#endif
- }
- else
+ if(buffer_size<=8)
+ return DC_CONTINUE;
+ i=UTFsize(&buffer[buffer_size/2+4], buffer_size/2-4)+4;
+ if(i<buffer_size/2)
{
- /* perl module */
- file_recovery_new->extension="pm";
- }
- return 1;
-}
-
-static int header_check_dc(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)
-{
- if(buffer[0]=='0' && buffer[1]=='0')
- { /*
- TSCe Survey Controller DC v10.0
- */
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="dc";
- return 1;
+ file_recovery->calculated_file_size=file_recovery->file_size+i;
+ return DC_STOP;
}
- return 0;
+ file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
+ file_recovery->data_check=&data_check_txt;
+ return DC_CONTINUE;
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_fods;
+ @ ensures valid_read_string((char*)file_recovery->filename);
+ @*/
static void file_rename_fods(file_recovery_t *file_recovery)
{
+ const char *meta_title="<office:meta><dc:title>";
FILE *file;
char buffer[4096];
- char *tmp;
+ char *tmp=NULL;
size_t lu;
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
if((file=fopen(file_recovery->filename, "rb"))==NULL)
+ {
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
+ }
if((lu=fread(&buffer, 1, sizeof(buffer)-1, file)) <= 0)
{
fclose(file);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
+ fclose(file);
buffer[lu]='\0';
- tmp=strchr(buffer,'<');
- while(tmp!=NULL)
+#ifndef __FRAMAC__
+ /*@
+ @ loop invariant tmp==\null || valid_read_string(tmp);
+ @ loop assigns tmp;
+ @*/
+ for(tmp=strchr(buffer,'<');
+ tmp!=NULL && strncasecmp(tmp, meta_title, 23)!=0;
+ tmp=strchr(tmp,'<'))
{
- if(strncasecmp(tmp, "<office:meta><dc:title>", 23)==0)
- {
- const char *title=tmp+23;
- tmp=strchr(title,'<');
- if(tmp!=NULL)
- *tmp='\0';
- file_rename(file_recovery, (const unsigned char*)title, strlen(title), 0, NULL, 1);
- fclose(file);
- return ;
- }
+ /* TODO assert tmp[0]=='<'; */
+ /*@ assert valid_read_string(tmp); */
tmp++;
- tmp=strchr(tmp,'<');
+ /*@ assert valid_read_string(tmp); */
}
- fclose(file);
+ if(tmp!=NULL)
+ {
+ const char *title=tmp+23;
+ /*@ assert valid_read_string(title); */
+ tmp=strchr(title,'<');
+ if(tmp!=NULL)
+ *tmp='\0';
+ file_rename(file_recovery, (const unsigned char*)title, strlen(title), 0, NULL, 1);
+ }
+#endif
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires valid_read_string((char*)file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_html;
+ @ ensures valid_read_string((char*)file_recovery->filename);
+ @*/
static void file_rename_html(file_recovery_t *file_recovery)
{
FILE *file;
char buffer[4096];
char *tmp;
size_t lu;
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
if((file=fopen(file_recovery->filename, "rb"))==NULL)
+ {
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
+ }
if((lu=fread(&buffer, 1, sizeof(buffer)-1, file)) <= 0)
{
fclose(file);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
+ fclose(file);
buffer[lu]='\0';
+#ifndef __FRAMAC__
tmp=strchr(buffer,'<');
while(tmp!=NULL)
{
if(strncasecmp(tmp, "</head", 5)==0)
{
- fclose(file);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
if(strncasecmp(tmp, "<title>", 7)==0)
@@ -690,294 +934,381 @@ static void file_rename_html(file_recovery_t *file_recovery)
if(tmp!=NULL)
*tmp='\0';
file_rename(file_recovery, (const unsigned char*)title, strlen(title), 0, NULL, 1);
- fclose(file);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
tmp++;
tmp=strchr(tmp,'<');
}
- fclose(file);
-}
-
-static int header_check_html(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)
-{
- if(file_recovery->file_stat!=NULL &&
- file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
- strcmp(file_recovery->extension,"mbox")==0)
- return 0;
- if(buffer[14]==0)
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_html;
- file_recovery_new->file_check=&file_check_size;
- /* Hypertext Markup Language (HTML) */
-#ifdef DJGPP
- file_recovery_new->extension="htm";
-#else
- file_recovery_new->extension="html";
#endif
- file_recovery_new->file_rename=&file_rename_html;
- return 1;
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
}
-static void file_check_vbm(file_recovery_t *file_recovery)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_emlx;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_emlx(file_recovery_t *file_recovery)
{
- file_search_footer(file_recovery, "</BackupMeta>", 13, 0);
- file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
+ if(file_recovery->file_size < file_recovery->calculated_file_size)
+ file_recovery->file_size=0;
+ else
+ {
+ if(file_recovery->file_size > file_recovery->calculated_file_size+2048)
+ file_recovery->file_size=file_recovery->calculated_file_size+2048;
+ file_search_footer(file_recovery, "</plist>\n", 9, 0);
+ }
}
-static int header_check_vbm(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_ers;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_ers(file_recovery_t *file_recovery)
{
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->extension="vbm";
- file_recovery_new->file_check=&file_check_vbm;
- return 1;
+ file_search_footer(file_recovery, "DatasetHeader End", 17, 0);
+ file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_gpx;
+ @ ensures \valid(file_recovery->handle);
+ @*/
static void file_check_gpx(file_recovery_t *file_recovery)
{
file_search_footer(file_recovery, "</gpx>", 6, 0);
file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
-static void file_check_xml(file_recovery_t *file_recovery)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_svg;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_svg(file_recovery_t *file_recovery)
{
- file_search_footer(file_recovery, ">", 1, 0);
+ file_search_footer(file_recovery, "</svg>", 6, 0);
file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
-static void file_check_svg(file_recovery_t *file_recovery)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_smil;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_smil(file_recovery_t *file_recovery)
{
- file_search_footer(file_recovery, "</svg>", 6, 0);
+ file_search_footer(file_recovery, "</smil>", 7, 0);
file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
-static data_check_t data_check_xml_utf8(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_vbm;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_vbm(file_recovery_t *file_recovery)
{
- unsigned int i;
- if(buffer_size<=8)
- return DC_CONTINUE;
- i=UTFsize(&buffer[buffer_size/2+4], buffer_size/2-4)+4;
- if(i<buffer_size/2)
- {
- file_recovery->calculated_file_size=file_recovery->file_size+i;
- return DC_STOP;
- }
- file_recovery->calculated_file_size=file_recovery->file_size+(buffer_size/2);
- file_recovery->data_check=&data_check_txt;
- return DC_CONTINUE;
+ file_search_footer(file_recovery, "</BackupMeta>", 13, 0);
+ file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
-static int header_check_xml_utf8(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
+ @ requires file_recovery->file_check == &file_check_xml;
+ @ ensures \valid(file_recovery->handle);
+ @*/
+static void file_check_xml(file_recovery_t *file_recovery)
{
- const char *tmp;
- /* buffer may not be null-terminated */
- char *buf=(char *)MALLOC(buffer_size+1);
- memcpy(buf, buffer, buffer_size);
- buf[buffer_size]='\0';
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_xml_utf8;
- file_recovery_new->extension=NULL;
- tmp=strchr(buf,'<');
- while(tmp!=NULL && file_recovery_new->extension==NULL)
- {
- if(strncasecmp(tmp, "<Archive name=\"Root\">", 8)==0)
- {
- /* Grasshopper archive */
- file_recovery_new->extension="ghx";
- }
- tmp++;
- tmp=strchr(tmp,'<');
- }
- if(file_recovery_new->extension==NULL)
- {
- file_recovery_new->extension="xml";
- }
- file_recovery_new->file_check=&file_check_xml;
- free(buf);
- return 1;
+ file_search_footer(file_recovery, ">", 1, 0);
+ file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
}
-static int header_check_xml_utf16(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == extension_dc);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
+ @ 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_dc(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)
{
- /* Avoid false positive with .sldprt */
- if(file_recovery->file_stat!=NULL &&
- file_recovery->file_stat->file_hint==&file_hint_doc)
+ if(buffer_size < 2)
+ return 0;
+ if(buffer[0]!='0' || buffer[1]!='0')
return 0;
+ /*
+ TSCe Survey Controller DC v10.0
+ */
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="xml";
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=extension_dc;
return 1;
}
-static int header_check_xml(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), file_recovery, file_recovery_new);
+ @ ensures \result == 1;
+ @ ensures file_recovery_new->file_stat == \null;
+ @ ensures file_recovery_new->handle == \null;
+ @ ensures file_recovery_new->calculated_file_size == 0;
+ @ ensures file_recovery_new->extension == extension_ers;
+ @ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
+ @ ensures file_recovery_new->data_check == &data_check_txt;
+ @ ensures file_recovery_new->file_check == &file_check_ers;
+ @ ensures file_recovery_new->file_rename == \null;
+ @ ensures valid_read_string(file_recovery_new->extension);
+ @ ensures \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
+static int header_check_ers(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
- const char *tmp;
- /* buffer may not be null-terminated */
- char *buf=(char *)MALLOC(buffer_size+1);
- memcpy(buf, buffer, buffer_size);
- buf[buffer_size]='\0';
+ /* ER Mapper Rasters (ERS) */
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->extension=NULL;
- tmp=strchr(buf,'<');
- while(tmp!=NULL && file_recovery_new->extension==NULL)
+ file_recovery_new->file_check=&file_check_ers;
+ file_recovery_new->extension=extension_ers;
+ return 1;
+}
+
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize > 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->extension != \null);
+ @ 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_fasttxt(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 txt_header_t *header=&fasttxt_headers[0];
+ /*@ loop unroll 200; */
+ while(header->len > 0)
{
- if(strncasecmp(tmp, "<Grisbi>", 8)==0)
- {
- /* Grisbi - Personal Finance Manager XML data */
- file_recovery_new->extension="gsb";
- }
- else if(strncasecmp(tmp, "<collection type=\"GC", 20)==0)
- {
- /* GCstart, personal collections manager, http://www.gcstar.org/ */
- file_recovery_new->extension="gcs";
- }
- else if(strncasecmp(tmp, "<html", 5)==0)
- {
- file_recovery_new->data_check=&data_check_html;
-#ifdef DJGPP
- file_recovery_new->extension="htm";
-#else
- file_recovery_new->extension="html";
-#endif
- file_recovery_new->file_rename=&file_rename_html;
- }
- else if(strncasecmp(tmp, "<Version>QBFSD", 14)==0)
- {
- /* QuickBook */
- file_recovery_new->extension="fst";
- }
- else if(strncasecmp(tmp, "<svg", 4)==0)
- {
- /* Scalable Vector Graphics */
- file_recovery_new->extension="svg";
- file_recovery_new->file_check=&file_check_svg;
- free(buf);
- return 1;
- }
- else if(strncasecmp(tmp, "<!DOCTYPE plist ", 16)==0)
- {
- /* Mac OS X property list */
-#ifdef DJGPP
- file_recovery_new->extension="pli";
-#else
- file_recovery_new->extension="plist";
-#endif
- }
- else if(strncasecmp(tmp, "<gpx ", 5)==0)
+ if(memcmp(buffer, header->string, header->len)==0)
{
- /* GPS eXchange Format */
- file_recovery_new->extension="gpx";
- file_recovery_new->file_check=&file_check_gpx;
- free(buf);
+ if(buffer[header->len]=='\0')
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ /*@ assert valid_read_string(header->extension); */
+ file_recovery_new->extension=header->extension;
+ /*@ assert file_recovery_new->extension != \null; */
+ file_recovery_new->min_filesize=header->len+1;
+ /*@ assert file_recovery_new->file_stat == \null; */
+ /*@ assert file_recovery_new->handle == \null; */
+ /*@ assert file_recovery_new->min_filesize > 0; */
+ /*@ assert file_recovery_new->calculated_file_size == 0; */
+ /*@ assert file_recovery_new->file_size == 0; */
+ /*@ assert file_recovery_new->data_check == &data_check_txt; */
+ /*@ assert file_recovery_new->file_check == &file_check_size; */
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ /*@ assert \separated(file_recovery_new, file_recovery_new->extension); */
return 1;
}
- else if(strncasecmp(tmp, "<PremiereData Version=", 22)==0)
- {
- /* Adobe Premiere project */
- file_recovery_new->data_check=NULL;
- file_recovery_new->extension="prproj";
- }
- else if(strncasecmp(tmp, "<SCRIBUS", 8)==0)
- {
- /* Scribus XML file */
- file_recovery_new->extension="sla";
- }
- else if(strncasecmp(tmp, "<FictionBook", 12)==0)
- {
- /* FictionBook, see http://www.fictionbook.org */
- file_recovery_new->extension="fb2";
- }
- else if(strncasecmp(tmp, "<office:document", 16)==0)
- {
- /* OpenDocument Flat XML Spreadsheet */
- file_recovery_new->extension="fods";
- file_recovery_new->data_check=NULL;
- file_recovery_new->file_rename=&file_rename_fods;
- }
- tmp++;
- tmp=strchr(tmp,'<');
- }
- if(file_recovery_new->extension==NULL)
- {
- /* XML Extensible Markup Language */
- file_recovery_new->extension="xml";
+ header++;
}
- file_recovery_new->file_check=&file_check_xml;
- free(buf);
- return 1;
+ return 0;
}
-static int header_check_rtf(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_html);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_html);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == &file_rename_html);
+ @ 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_html(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)
{
- unsigned int i;
- for(i=0; i<16; i++)
- if(buffer[i]=='\0')
- return 0;
- /* Avoid a false positive with .snt */
+ if(buffer_size < 15)
+ return 0;
if(file_recovery->file_stat!=NULL &&
- file_recovery->file_stat->file_hint==&file_hint_doc)
+ file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
+ file_recovery->extension==extension_mbox)
+ return 0;
+ if(buffer[14]==0)
return 0;
reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->data_check=&data_check_html;
file_recovery_new->file_check=&file_check_size;
- /* Rich Text Format */
- file_recovery_new->extension="rtf";
+ /* Hypertext Markup Language (HTML) */
+ file_recovery_new->extension=extension_html;
+ file_recovery_new->file_rename=&file_rename_html;
return 1;
}
-static int header_check_xmp(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_ics);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_ics(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)
{
- if(buffer[35]=='\0')
+ const char *date_asc;
+ char *buffer2;
+ if(buffer_size < 22)
return 0;
- if(file_recovery->file_stat!=NULL &&
- (file_recovery->file_stat->file_hint==&file_hint_jpg ||
- file_recovery->file_stat->file_hint==&file_hint_pdf ||
- file_recovery->file_stat->file_hint==&file_hint_tiff))
+ if(buffer[15]=='\0')
return 0;
- /* Adobe's Extensible Metadata Platform */
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="xmp";
- return 1;
-}
-
-static void file_check_thunderbird(file_recovery_t *file_recovery)
-{
- if(file_recovery->file_size<file_recovery->calculated_file_size)
+ /* vcalendar */
+ file_recovery_new->extension=extension_ics;
+ /* DTSTART:19970714T133000 ;Local time
+ * DTSTART:19970714T173000Z ;UTC time
+ * DTSTART;TZID=US-Eastern:19970714T133000 ;Local time and time
+ */
+ buffer2=(char *)MALLOC(buffer_size+1);
+ buffer2[buffer_size]='\0';
+ memcpy(buffer2, buffer, buffer_size);
+ date_asc=strstr(buffer2, "DTSTART");
+ if(date_asc!=NULL)
+ date_asc=strchr(date_asc, ':');
+ if(date_asc!=NULL && date_asc+1+14 < buffer2+buffer_size)
{
- file_recovery->file_size=0;
- return;
+ file_recovery_new->time=get_time_from_YYYYMMDD_HHMMSS(date_asc+1);
}
- file_recovery->file_size=file_recovery->calculated_file_size;
+ free(buffer2);
+ return 1;
}
-static int header_check_thunderbird(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)
+#ifdef UTF16
+static int header_check_le16_txt(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)
{
unsigned int i;
- if(file_recovery->file_stat!=NULL &&
- file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
- strcmp(file_recovery->extension,"mbox")==0)
- return 0;
- for(i=0; i<64; i++)
- if(buffer[i]==0)
- return 0;
+ for(i=0; i+1 < buffer_size; i+=2)
+ {
+ if(!( buffer[i+1]=='\0' && (isprint(buffer[i]) || buffer[i]=='\n' || buffer[i]=='\r' || buffer[i]==0xbb)))
+ {
+ if(i<40)
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->calculated_file_size=i;
+ file_recovery_new->data_check=&data_check_size;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=extension_utf16;
+ return 1;
+ }
+ }
reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_thunderbird;
- file_recovery_new->extension="mbox";
+ file_recovery_new->calculated_file_size=i;
+ file_recovery_new->data_check=&data_check_size;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=extension_utf16;
return 1;
}
+#endif
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_mbox);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_mbox(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)
{
unsigned int i;
+ if(buffer_size < 200)
+ return 0;
if(file_recovery->file_stat!=NULL &&
file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
- strcmp(file_recovery->extension,"mbox")==0)
+ file_recovery->extension==extension_mbox)
return 0;
+ /*@ loop assigns i; */
for(i=0; i<64; i++)
if(buffer[i]==0)
return 0;
@@ -985,6 +1316,7 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
memcmp(buffer, "From MAILER-DAEMON ", 19)!=0)
{
/* From someone@somewhere */
+ /*@ loop assigns i; */
for(i=5; i<200 && buffer[i]!=' ' && buffer[i]!='@'; i++);
if(buffer[i]!='@')
return 0;
@@ -993,114 +1325,365 @@ static int header_check_mbox(const unsigned char *buffer, const unsigned int buf
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Incredimail has .imm extension but this extension isn't frequent */
- file_recovery_new->extension="mbox";
+ file_recovery_new->extension=extension_mbox;
return 1;
}
-static int header_check_fasttxt(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_java || file_recovery_new->extension == extension_pm);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_perlm(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 txt_header_t *header=&fasttxt_headers[0];
- while(header->len > 0)
+ unsigned int i;
+ const unsigned int buffer_size_test=(buffer_size < 2048 ? buffer_size : 2048);
+ if(buffer_size < 128)
+ return 0;
+ for(i=0; i<128 && buffer[i]!=';' && buffer[i]!='\n'; i++);
+ if(buffer[i]!=';')
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ if( td_memmem(buffer, buffer_size_test, "class", 5)!=NULL ||
+ td_memmem(buffer, buffer_size_test, "private static", 14)!=NULL ||
+ td_memmem(buffer, buffer_size_test, "public interface", 16)!=NULL)
{
- if(memcmp(buffer, header->string, header->len)==0)
- {
- if(buffer[header->len]=='\0')
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension=header->extension;
- file_recovery_new->min_filesize=header->len+1;
- return 1;
- }
- header++;
+ /* source code in java */
+ file_recovery_new->extension=extension_java;
}
- return 0;
+ else
+ {
+ /* perl module */
+ file_recovery_new->extension=extension_pm;
+ }
+ return 1;
}
-static int is_ini(const char *buffer)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_rtf);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_rtf(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
- const char *src=buffer;
- if(*src!='[')
+ unsigned int i;
+ if(buffer_size < 16)
return 0;
- src++;
- while(1)
- {
- if(*src==']')
- {
- if(src > buffer + 3)
- return 1;
- return 0;
- }
- if(!isalnum(*src) && *src!=' ')
+ for(i=0; i<16; i++)
+ if(buffer[i]=='\0')
return 0;
- src++;
- }
+ /* Avoid a false positive with .snt */
+ if(file_recovery->file_stat!=NULL
+#if !defined(MAIN_txt)
+ && file_recovery->file_stat->file_hint==&file_hint_doc
+#endif
+ )
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ /* Rich Text Format */
+ file_recovery_new->extension=extension_rtf;
+ return 1;
}
-#ifdef UTF16
-static int header_check_le16_txt(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_smil);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_smil);
+ @ 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_smil(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)
+{
+ /* Synchronized Multimedia Integration Language
+ * http://en.wikipedia.org/wiki/Synchronized_Multimedia_Integration_Language */
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_smil;
+ file_recovery_new->extension=extension_smil;
+ return 1;
+}
+
+/*@
+ @ requires buffer_size > 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->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_snz, buffer+(..), 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->extension == file_hint_snz.extension);
+ @ 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 == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_snz(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+{
+ const unsigned int buffer_size_test=(buffer_size < 512? buffer_size : 512);
+ const unsigned char *pos=(const unsigned char *)td_memmem(buffer, buffer_size_test, ".snz", 4);
+ if(pos==NULL)
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=file_hint_snz.extension;
+ file_recovery_new->min_filesize=pos-buffer;
+ return 1;
+}
+
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_stl);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_stl(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+{
+ const unsigned int buffer_size_test=(buffer_size < 512? buffer_size : 512);
+ if(td_memmem(buffer, buffer_size_test, "facet normal", 12)==NULL)
+ return 0;
+ /* StereoLithography - STL Ascii format
+ * http://www.ennex.com/~fabbers/StL.asp */
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=extension_stl;
+ return 1;
+}
+
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_svg);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_svg);
+ @ 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_svg(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)
+{
+ /* Scalable Vector Graphics */
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->extension=extension_svg;
+ file_recovery_new->file_check=&file_check_svg;
+ return 1;
+}
+
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_mbox);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_thunderbird(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)
{
unsigned int i;
- for(i=0; i+1 < buffer_size; i+=2)
- {
- if(!( buffer[i+1]=='\0' && (isprint(buffer[i]) || buffer[i]=='\n' || buffer[i]=='\r' || buffer[i]==0xbb)))
- {
- if(i<40)
- return 0;
- reset_file_recovery(file_recovery_new);
- file_recovery_new->calculated_file_size=i;
- file_recovery_new->data_check=&data_check_size;
- file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="utf16";
- return 1;
- }
- }
+ if(buffer_size < 64)
+ return 0;
+ if(file_recovery->file_stat!=NULL &&
+ file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
+ file_recovery->extension == extension_mbox)
+ return 0;
+ /*@ loop assigns i; */
+ for(i=0; i<64; i++)
+ if(buffer[i]==0)
+ return 0;
reset_file_recovery(file_recovery_new);
- file_recovery_new->calculated_file_size=i;
- file_recovery_new->data_check=&data_check_size;
+ file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="utf16";
+ file_recovery_new->extension=extension_mbox;
return 1;
}
-#endif
-static void file_check_emlx(file_recovery_t *file_recovery)
+/*@
+ @ 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_fasttxt, buffer+(..), 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->extension == extension_ttd);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_ttd);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_ttd(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)
{
- if(file_recovery->file_size < file_recovery->calculated_file_size)
- file_recovery->file_size=0;
- else
- {
- if(file_recovery->file_size > file_recovery->calculated_file_size+2048)
- file_recovery->file_size=file_recovery->calculated_file_size+2048;
- file_search_footer(file_recovery, "</plist>\n", 9, 0);
- }
+ if(buffer[56]<'0' || buffer[56]>'9')
+ return 0;
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_ttd;
+ file_recovery_new->file_check=&file_check_size;
+ file_recovery_new->extension=extension_ttd;
+ /*@ assert valid_read_string(file_recovery_new->extension); */
+ /*@ assert \separated(file_recovery_new, file_recovery_new->extension); */
+ return 1;
}
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension != \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null || file_recovery_new->data_check == &data_check_html || file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_emlx || file_recovery_new->file_check == &file_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null || file_recovery_new->file_rename == &file_rename_html);
+ @ 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_txt(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 char *buffer_lower=NULL;
static unsigned int buffer_lower_size=0;
unsigned int l;
const unsigned int buffer_size_test=(buffer_size < 2048 ? buffer_size : 2048);
+ if(buffer_size < 512)
+ return 0;
{
unsigned int i;
- unsigned int tmp=0;
+ uint64_t tmp=0;
+ /*@
+ @ loop unroll 10;
+ @ loop invariant 0 <= i <= 10;
+ @ loop assigns i, tmp;
+ @ loop variant 10-i;
+ @*/
for(i=0;i<10 && isdigit(buffer[i]);i++)
- tmp=tmp*10+buffer[i]-'0';
+ {
+ /*@ assert '0' <= buffer[i] <= '9'; */
+ unsigned int v=buffer[i]-'0';
+ /*@ assert 0 <= v <= 9; */
+ tmp=tmp*10+v;
+ }
if(buffer[i]==0x0a &&
(memcmp(buffer+i+1, "Return-Path: ", 13)==0 ||
memcmp(buffer+i+1, "Received: from", 14)==0) &&
!(file_recovery->file_stat!=NULL &&
file_recovery->file_stat->file_hint==&file_hint_fasttxt &&
- strcmp(file_recovery->extension,"mbox")==0))
+ file_recovery->extension==extension_mbox))
{
reset_file_recovery(file_recovery_new);
file_recovery_new->calculated_file_size=tmp+i+1;
file_recovery_new->data_check=NULL;
file_recovery_new->file_check=&file_check_emlx;
/* Mac OSX mail */
- file_recovery_new->extension="emlx";
+ file_recovery_new->extension=extension_emlx;
return 1;
}
}
@@ -1112,7 +1695,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Dos/Windows batch */
- file_recovery_new->extension="bat";
+ file_recovery_new->extension=extension_bat;
return 1;
}
if(strncasecmp((const char *)buffer, "<%@ language=\"vbscript", 22)==0)
@@ -1123,7 +1706,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Microsoft Active Server Pages */
- file_recovery_new->extension="asp";
+ file_recovery_new->extension=extension_asp;
return 1;
}
if(strncasecmp((const char *)buffer, "version 4.00\r\nbegin", 19)==0)
@@ -1134,7 +1717,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Microsoft Visual Basic */
- file_recovery_new->extension="vb";
+ file_recovery_new->extension=extension_vb;
return 1;
}
if(strncasecmp((const char *)buffer, "begin:vcard", 11)==0)
@@ -1145,7 +1728,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* vcard, electronic business cards */
- file_recovery_new->extension="vcf";
+ file_recovery_new->extension=extension_vcf;
return 1;
}
if(buffer[0]=='#' && buffer[1]=='!')
@@ -1156,13 +1739,31 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
res=(const unsigned char *)memchr(haystack,'\n',ll);
if(res!=NULL)
ll=res-haystack;
+ if(td_memmem(haystack, ll, "groovy", 6) != NULL)
+ {
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ /* Groovy script */
+ file_recovery_new->extension=extension_groovy;
+ return 1;
+ }
if(td_memmem(haystack, ll, "perl", 4) != NULL)
{
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Perl script */
- file_recovery_new->extension="pl";
+ file_recovery_new->extension=extension_pl;
+ return 1;
+ }
+ if(td_memmem(haystack, ll, "php", 3) != NULL)
+ {
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->file_check=&file_check_size;
+ /* PHP script */
+ file_recovery_new->extension=extension_php;
return 1;
}
if(td_memmem(haystack, ll, "python", 6) != NULL)
@@ -1171,7 +1772,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Python script */
- file_recovery_new->extension="py";
+ file_recovery_new->extension=extension_py;
return 1;
}
if(td_memmem(haystack, ll, "ruby", 4) != NULL)
@@ -1180,7 +1781,7 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Ruby script */
- file_recovery_new->extension="rb";
+ file_recovery_new->extension=extension_rb;
return 1;
}
}
@@ -1213,25 +1814,15 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
l=UTF2Lat((unsigned char*)buffer_lower, buffer, buffer_size_test);
if(l<10)
return 0;
- {
- unsigned int line_nbr=0;
- unsigned int i;
- for(i=0; i<512 && i<l; i++)
- {
- if(buffer[i]=='\n')
- line_nbr++;
- }
- /* A text file must contains several lines */
- if(line_nbr==0)
- return 0;
- }
+ if(has_newline(buffer_lower, l)==0)
+ return 0;
if(strncasecmp((const char *)buffer, "rem ", 4)==0)
{
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
/* Dos/Windows batch */
- file_recovery_new->extension="bat";
+ file_recovery_new->extension=extension_bat;
return 1;
}
if(strncasecmp((const char *)buffer, "dn: ", 4)==0)
@@ -1239,152 +1830,115 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="ldif";
+ file_recovery_new->extension=extension_ldif;
return 1;
}
{
const char *ext=NULL;
- /* ind=~0: random
- * ind=~1: constant */
- double ind;
- unsigned int nbrf=0;
- unsigned int is_csv=1;
- char *str;
- /* Detect Fortran */
- {
- str=buffer_lower;
- while((str=strstr(str, "\n "))!=NULL)
- {
- nbrf++;
- str++;
- }
- }
- /* Detect csv */
- {
- unsigned int csv_per_line_current=0;
- unsigned int csv_per_line=0;
- unsigned int line_nbr=0;
- unsigned int i;
- for(i=0;i<l && is_csv>0;i++)
- {
- if(buffer_lower[i]==';')
- {
- csv_per_line_current++;
- }
- else if(buffer_lower[i]=='\n')
- {
- if(line_nbr==0)
- csv_per_line=csv_per_line_current;
- if(csv_per_line_current!=csv_per_line)
- is_csv=0;
- line_nbr++;
- csv_per_line_current=0;
- }
- }
- if(csv_per_line<1 || line_nbr<10)
- is_csv=0;
- }
- /* if(l>1) */
- {
- unsigned int stats[256];
- unsigned int i;
- memset(&stats, 0, sizeof(stats));
- for(i=0;i<l;i++)
- stats[(unsigned char)buffer_lower[i]]++;
- ind=0;
- for(i=0;i<256;i++)
- if(stats[i]>0)
- ind+=stats[i]*(stats[i]-1);
- ind=ind/l/(l-1);
- }
+ /* ind_random=~0: random
+ * ind_random=~1: constant */
+ double ind_random;
+ const char *str;
+ ind_random=is_random((const unsigned char *)buffer_lower, l);
/* Windows Autorun */
if(strstr(buffer_lower, "[autorun]")!=NULL)
- ext="inf";
+ {
+ ext=extension_inf;
+ log_info("ext=%s\n", ext);
+ }
/* Detect .ini */
- else if(buffer[0]=='[' && l>50 && is_ini(buffer_lower))
- ext="ini";
+ else if(buffer[0]=='[' && l>50 && is_ini((const unsigned char *)buffer_lower))
+ ext=extension_ini;
/* php (Hypertext Preprocessor) script */
else if(strstr(buffer_lower, "<?php")!=NULL)
- ext="php";
+ ext=extension_php;
/* Comma separated values */
- else if(is_csv>0)
- ext="csv";
+ else if(is_csv(buffer_lower, l)!=0)
+ ext=extension_csv;
/* Detect LaTeX, C, PHP, JSP, ASP, HTML, C header */
else if(strstr(buffer_lower, "\\begin{")!=NULL)
- ext="tex";
+ ext=extension_tex;
else if(strstr(buffer_lower, "#include")!=NULL)
- ext="c";
+ ext=extension_c;
else if(l>20 && strstr(buffer_lower, "<%@")!=NULL)
- ext="jsp";
+ ext=extension_jsp;
else if(l>20 && strstr(buffer_lower, "<%=")!=NULL)
- ext="jsp";
+ ext=extension_jsp;
else if(l>20 && strstr(buffer_lower, "<% ")!=NULL)
- ext="asp";
+ ext=extension_asp;
else if(strstr(buffer_lower, "<html")!=NULL)
- ext="html";
+ ext=extension_html;
else if(strstr(buffer_lower, "private static")!=NULL ||
strstr(buffer_lower, "public interface")!=NULL)
{
-#ifdef DJGPP
- ext="jav";
-#else
- ext="java";
-#endif
+ ext=extension_java;
}
else if(strstr(buffer_lower, "\nimport (")!=NULL)
{
- ext="go";
+ ext=extension_go;
}
else if((str=strstr(buffer_lower, "\nimport "))!=NULL)
{
+ /*@ assert valid_read_string(str); */
+#ifndef __FRAMAC__
str+=8;
+#endif
+ /*@ assert valid_read_string(str); */
+ /*@
+ @ loop assigns str;
+ @*/
while(*str!='\0' && *str!='\n' && *str!=';')
str++;
if(*str==';')
- ext="java";
+ ext=extension_java;
else
- ext="py";
+ ext=extension_py;
}
else if(strstr(buffer_lower, "class ")!=NULL &&
(l>=100 || file_recovery->file_stat==NULL))
{
-#ifdef DJGPP
- ext="jav";
-#else
- ext="java";
-#endif
+ ext=extension_java;
}
/* Fortran */
- else if(nbrf>10 && ind<0.9 && strstr(buffer_lower, "integer")!=NULL)
- ext="f";
+ else if(ind_random<0.9 && is_fortran(buffer_lower)!=0)
+ ext=extension_f;
/* LilyPond http://lilypond.org*/
else if(strstr(buffer_lower, "\\score {")!=NULL)
- ext="ly";
+ ext=extension_ly;
/* C header file */
else if(strstr(buffer_lower, "/*")!=NULL && l>50)
- ext="h";
- else if(l<100 || ind<0.03 || ind>0.90)
+ ext=extension_h;
+ else if(l<100 || ind_random<0.03 || ind_random>0.90)
ext=NULL;
/* JavaScript Object Notation */
else if(memcmp(buffer_lower, "{\"", 2)==0)
- ext="json";
+ ext=extension_json;
+ else if(strstr(buffer_lower,"<br>")!=NULL || strstr(buffer_lower,"<p>")!=NULL)
+ ext=extension_html;
else
ext=file_hint_txt.extension;
if(ext==NULL)
return 0;
- if(strcmp(ext,"txt")==0 &&
- (strstr(buffer_lower,"<br>")!=NULL || strstr(buffer_lower,"<p>")!=NULL))
- {
- ext="html";
- }
if(file_recovery->file_stat!=NULL)
{
- if(file_recovery->file_stat->file_hint == &file_hint_doc)
+ if(file_recovery->file_stat->file_hint == &file_hint_fasttxt ||
+ file_recovery->file_stat->file_hint == &file_hint_txt)
+ {
+ /* file_recovery->filename is a .html */
+ buffer_lower[511]='\0';
+ if(strstr(buffer_lower, "<html")==NULL)
+ return 0;
+ /* Special case: two consecutive HTML files */
+ }
+ else
+#if !defined(MAIN_txt)
+ if(file_recovery->file_stat->file_hint == &file_hint_doc)
+#endif
{
unsigned int i;
unsigned int txt_nl=0;
/* file_recovery->filename is .doc */
- if(ind>0.20)
+ if(ind_random>0.20)
return 0;
/* Unix: \n (0xA)
* Dos: \r\n (0xD 0xA)
@@ -1400,18 +1954,9 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
if(txt_nl<=1)
return 0;
}
- else if(file_recovery->file_stat->file_hint == &file_hint_fasttxt ||
- file_recovery->file_stat->file_hint == &file_hint_txt)
- {
- /* file_recovery->filename is a .html */
- buffer_lower[511]='\0';
- if(strstr(buffer_lower, "<html")==NULL)
- return 0;
- /* Special case: two consecutive HTML files */
- }
}
reset_file_recovery(file_recovery_new);
- if(strcmp(ext, "html")==0)
+ if(ext==extension_html)
{
file_recovery_new->file_rename=&file_rename_html;
file_recovery_new->data_check=&data_check_html;
@@ -1424,66 +1969,305 @@ static int header_check_txt(const unsigned char *buffer, const unsigned int buff
}
}
-static void file_check_smil(file_recovery_t *file_recovery)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_vbm);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_vbm);
+ @ 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_vbm(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)
{
- file_search_footer(file_recovery, "</smil>", 7, 0);
- file_allow_nl(file_recovery, NL_BARENL|NL_CRLF|NL_BARECR);
+ reset_file_recovery(file_recovery_new);
+ file_recovery_new->data_check=&data_check_txt;
+ file_recovery_new->extension=extension_vbm;
+ file_recovery_new->file_check=&file_check_vbm;
+ return 1;
}
-static int header_check_smil(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), file_recovery, file_recovery_new);
+ @ ensures \result == 1;
+ @ ensures file_recovery_new->file_stat == \null;
+ @ ensures file_recovery_new->handle == \null;
+ @ ensures file_recovery_new->calculated_file_size == 0;
+ @ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
+ @ ensures file_recovery_new->data_check == \null ||
+ file_recovery_new->data_check == data_check_html ||
+ file_recovery_new->data_check == data_check_txt;
+ @ ensures file_recovery_new->file_check == \null ||
+ file_recovery_new->file_check == &file_check_gpx ||
+ file_recovery_new->file_check == &file_check_svg ||
+ file_recovery_new->file_check == &file_check_xml;
+ @ ensures file_recovery_new->file_rename == \null ||
+ file_recovery_new->file_rename == &file_rename_fods ||
+ file_recovery_new->file_rename == &file_rename_html;
+ @ ensures valid_read_string(file_recovery_new->extension);
+ @ ensures \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
+static int header_check_xml(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)
{
- /* Synchronized Multimedia Integration Language
- * http://en.wikipedia.org/wiki/Synchronized_Multimedia_Integration_Language */
+ const char *tmp;
+ /* buffer may not be null-terminated */
+ char *buf=(char *)MALLOC(buffer_size+1);
+ memcpy(buf, buffer, buffer_size);
+ buf[buffer_size]='\0';
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_smil;
- file_recovery_new->extension="smil";
+ file_recovery_new->file_check=&file_check_xml;
+ file_recovery_new->extension=NULL;
+ tmp=strchr(buf,'<');
+ while(tmp!=NULL)
+ {
+ if(strncasecmp(tmp, "<Grisbi>", 8)==0)
+ {
+ /* Grisbi - Personal Finance Manager XML data */
+ file_recovery_new->extension=extension_gsb;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<collection type=\"GC", 20)==0)
+ {
+ /* GCstart, personal collections manager, http://www.gcstar.org/ */
+ file_recovery_new->extension=extension_gcs;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<html", 5)==0)
+ {
+ file_recovery_new->data_check=&data_check_html;
+ file_recovery_new->extension=extension_html;
+ file_recovery_new->file_rename=&file_rename_html;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<Version>QBFSD", 14)==0)
+ {
+ /* QuickBook */
+ file_recovery_new->extension=extension_fst;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<svg", 4)==0)
+ {
+ /* Scalable Vector Graphics */
+ file_recovery_new->extension=extension_svg;
+ file_recovery_new->file_check=&file_check_svg;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<!DOCTYPE plist ", 16)==0)
+ {
+ /* Mac OS X property list */
+ file_recovery_new->extension=extension_plist;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<gpx ", 5)==0)
+ {
+ /* GPS eXchange Format */
+ file_recovery_new->extension=extension_gpx;
+ file_recovery_new->file_check=&file_check_gpx;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<PremiereData Version=", 22)==0)
+ {
+ /* Adobe Premiere project */
+ file_recovery_new->data_check=NULL;
+ file_recovery_new->extension=extension_prproj;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<SCRIBUS", 8)==0)
+ {
+ /* Scribus XML file */
+ file_recovery_new->extension=extension_sla;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<FictionBook", 12)==0)
+ {
+ /* FictionBook, see http://www.fictionbook.org */
+ file_recovery_new->extension=extension_fb2;
+ free(buf);
+ return 1;
+ }
+ else if(strncasecmp(tmp, "<office:document", 16)==0)
+ {
+ /* OpenDocument Flat XML Spreadsheet */
+ file_recovery_new->extension=extension_fods;
+ file_recovery_new->data_check=NULL;
+ file_recovery_new->file_rename=&file_rename_fods;
+ free(buf);
+ return 1;
+ }
+ tmp++;
+ tmp=strchr(tmp,'<');
+ }
+ /* XML Extensible Markup Language */
+ file_recovery_new->extension=extension_xml;
+ free(buf);
return 1;
}
-static int header_check_stl(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), file_recovery, file_recovery_new);
+ @ ensures \result == 1;
+ @ ensures file_recovery_new->file_stat == \null;
+ @ ensures file_recovery_new->handle == \null;
+ @ ensures file_recovery_new->extension == extension_ghx || file_recovery_new->extension == extension_xml;
+ @ ensures file_recovery_new->calculated_file_size == 0;
+ @ ensures file_recovery_new->file_size == 0;
+ @ ensures file_recovery_new->min_filesize == 0;
+ @ ensures (buffer_size >= 10) ==> (file_recovery_new->data_check == &data_check_xml_utf8);
+ @ ensures (buffer_size < 10) ==> file_recovery_new->data_check == \null;
+ @ ensures file_recovery_new->file_check == &file_check_xml;
+ @ ensures valid_read_string(file_recovery_new->extension);
+ @ ensures \separated(file_recovery_new, file_recovery_new->extension);
+ @*/
+static int header_check_xml_utf8(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
- const unsigned int buffer_size_test=(buffer_size < 512? buffer_size : 512);
- if(td_memmem(buffer, buffer_size_test, "facet normal", 12)==NULL)
- return 0;
- /* StereoLithography - STL Ascii format
- * http://www.ennex.com/~fabbers/StL.asp */
+ const char *tmp;
+ /* buffer may not be null-terminated */
+ char *buf=(char *)MALLOC(buffer_size+1);
+ memcpy(buf, buffer, buffer_size);
+ buf[buffer_size]='\0';
reset_file_recovery(file_recovery_new);
- file_recovery_new->data_check=&data_check_txt;
- file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="stl";
+ if(buffer_size >= 10)
+ file_recovery_new->data_check=&data_check_xml_utf8;
+ file_recovery_new->extension=NULL;
+ tmp=strchr(buf,'<');
+ /*@
+ @ loop assigns tmp,file_recovery_new->extension;
+ @*/
+ while(tmp!=NULL && file_recovery_new->extension==NULL)
+ {
+ if(strncasecmp(tmp, "<Archive name=\"Root\">", 8)==0)
+ {
+ /* Grasshopper archive */
+ file_recovery_new->extension=extension_ghx;
+ }
+ tmp++;
+ tmp=strchr(tmp,'<');
+ }
+ if(file_recovery_new->extension==NULL)
+ {
+ file_recovery_new->extension=extension_xml;
+ }
+ file_recovery_new->file_check=&file_check_xml;
+ free(buf);
return 1;
}
-static int header_check_svg(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_xml);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == \null);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == \null);
+ @ 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_xml_utf16(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)
{
- /* Scalable Vector Graphics */
+ /* Avoid false positive with .sldprt */
+ if(file_recovery->file_stat!=NULL
+#if !defined(MAIN_txt)
+ && file_recovery->file_stat->file_hint==&file_hint_doc
+#endif
+ )
+ return 0;
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension="svg";
- file_recovery_new->file_check=&file_check_svg;
+ file_recovery_new->extension=extension_xml;
return 1;
}
-static int header_check_snz(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
+/*@
+ @ requires buffer_size > 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->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_fasttxt, buffer+(..), 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->extension == extension_xmp);
+ @ 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->min_filesize == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_txt);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @ 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_xmp(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
- const unsigned int buffer_size_test=(buffer_size < 512? buffer_size : 512);
- const unsigned char *pos=(const unsigned char *)td_memmem(buffer, buffer_size_test, ".snz", 4);
- if(pos==NULL)
+ if(buffer[35]=='\0')
+ return 0;
+ if(file_recovery->file_stat!=NULL
+#if !defined(MAIN_txt)
+ && (file_recovery->file_stat->file_hint==&file_hint_jpg ||
+ file_recovery->file_stat->file_hint==&file_hint_pdf ||
+ file_recovery->file_stat->file_hint==&file_hint_tiff)
+#endif
+ )
return 0;
+ /* Adobe's Extensible Metadata Platform */
reset_file_recovery(file_recovery_new);
file_recovery_new->data_check=&data_check_txt;
file_recovery_new->file_check=&file_check_size;
- file_recovery_new->extension="snz";
- file_recovery_new->min_filesize=pos-buffer;
+ file_recovery_new->extension=extension_xmp;
return 1;
}
-static void register_header_check_snz(file_stat_t *file_stat)
-{
- register_header_check(0, "DEFAULT\n", 8, &header_check_snz, file_stat);
- register_header_check(0, "DEFAULT\r\n", 9, &header_check_snz, file_stat);
-}
-
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_fasttxt(file_stat_t *file_stat)
{
static const unsigned char header_xml_utf8[17] = {0xef, 0xbb, 0xbf, '<', '?', 'x', 'm', 'l', ' ', 'v', 'e', 'r', 's', 'i', 'o', 'n', '='};
@@ -1491,6 +2275,7 @@ static void register_header_check_fasttxt(file_stat_t *file_stat)
const txt_header_t *header=&fasttxt_headers[0];
while(header->len > 0)
{
+ assert(strlen(header->string) == header->len);
register_header_check(0, header->string, header->len, &header_check_fasttxt, file_stat);
header++;
}
@@ -1524,3 +2309,1815 @@ static void register_header_check_fasttxt(file_stat_t *file_stat)
register_header_check(0, "<x:xmpmeta xmlns:x=\"adobe:ns:meta/\"", 35, &header_check_xmp, file_stat);
register_header_check(0, "<svg xmlns=\"http://www.w3.org/2000/svg\"", 39, &header_check_svg, file_stat);
}
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
+static void register_header_check_snz(file_stat_t *file_stat)
+{
+ register_header_check(0, "DEFAULT\n", 8, &header_check_snz, file_stat);
+ register_header_check(0, "DEFAULT\r\n", 9, &header_check_snz, file_stat);
+}
+
+/*@
+ @ requires \valid(file_stat);
+ @*/
+static void register_header_check_txt(file_stat_t *file_stat)
+{
+ unsigned int i;
+ for(i=0; i<256; i++)
+ ascii_char[i]=i;
+ for(i=0; i<256; i++)
+ {
+ if(filtre(i) || i==0xE2 || i==0xC2 || i==0xC3 || i==0xC5 || i==0xC6 || i==0xCB)
+ register_header_check(0, &ascii_char[i], 1, &header_check_txt, file_stat);
+ }
+#ifdef UTF16
+ register_header_check(1, &ascii_char[0], 1, &header_check_le16_txt, file_stat);
+#endif
+}
+
+#if defined(MAIN_txt)
+#define BLOCKSIZE 65536u
+static int main_dc()
+{
+ const char fn[] = "recup_dir.1/f0000000.dc";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_dc(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.extension == extension_dc; */
+ /*@ assert valid_read_string(extension_dc); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_rename == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.extension == extension_dc; */
+ /*@ assert valid_read_string(extension_dc); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_dc(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_ers()
+{
+ const char fn[] = "recup_dir.1/f0000000.ers";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_ers(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.extension == extension_ers; */
+ /*@ assert valid_read_string(extension_ers); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_ers; */
+ /*@ assert file_recovery_new.file_rename == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.extension == extension_ers; */
+ /*@ assert valid_read_string(extension_ers); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_ers(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_ers; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_ers(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_fasttxt()
+{
+ const char fn[] = "recup_dir.1/f0000000.txt";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_fasttxt(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ /*@ assert file_recovery_new.extension != \null; */
+ 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 valid_read_string((char *)file_recovery_new.extension); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_rename == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_fasttxt(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_html()
+{
+ const char fn[] = "recup_dir.1/f0000000.html";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_html(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.extension == extension_html; */
+ /*@ assert valid_read_string(extension_html); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_html; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_rename == &file_rename_html; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_html; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_html(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_html; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_html(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.extension == extension_html; */
+ /*@ assert valid_read_string(extension_html); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_html(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ file_rename_html(&file_recovery_new);
+ return 0;
+}
+
+static int main_ics()
+{
+ const char fn[] = "recup_dir.1/f0000000.ics";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_ics(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.extension == extension_ics; */
+ /*@ assert valid_read_string(extension_ics); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.extension == extension_ics; */
+ /*@ assert valid_read_string(extension_ics); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_ics(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_mbox()
+{
+ const char fn[] = "recup_dir.1/f0000000.mbox";
+ 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.extension == \null; */
+ /*@ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_mbox(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.extension == extension_mbox; */
+ /*@ assert valid_read_string(extension_mbox); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert file_recovery_new.extension == extension_mbox; */
+ /*@ assert valid_read_string(extension_mbox); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_mbox(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_perlm()
+{
+ const char fn[] = "recup_dir.1/f0000000.pm";
+ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_perlm(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_pm || file_recovery_new.extension == extension_java; */
+ /*@ assert valid_read_string((char *)file_recovery_new.extension); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_perlm(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_rtf()
+{
+ const char fn[] = "recup_dir.1/f0000000.rtf";
+ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_rtf(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_rtf; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_rtf(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_smail()
+{
+ const char fn[] = "recup_dir.1/f0000000.smil";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_smil(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_smil; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_smil; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_smil(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_smil; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_smil(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_snz()
+{
+ const char fn[] = "recup_dir.1/f0000000.snz";
+ 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_snz;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_snz(&file_stats);
+#endif
+ if(header_check_snz(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == file_hint_snz.extension; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_snz; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_snz(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_stl()
+{
+ const char fn[] = "recup_dir.1/f0000000.stl";
+ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_stl(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_stl; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_stl(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_svg()
+{
+ const char fn[] = "recup_dir.1/f0000000.svg";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_svg(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_svg; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_svg; */
+ /*@ assert file_recovery_new.data_check == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_svg(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_svg; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_svg(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_thunderbird()
+{
+ const char fn[] = "recup_dir.1/f0000000.mbox";
+ 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);
+ reset_file_recovery(&file_recovery_new);
+ /*@ assert file_recovery.file_stat == \null; */
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_stats.file_hint=&file_hint_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_thunderbird(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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(extension_mbox); */
+ /*@ assert file_recovery_new.extension == extension_mbox; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string(extension_mbox); */
+ /*@ assert file_recovery_new.extension == extension_mbox; */
+ /*@ assert valid_read_string(file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_thunderbird(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_ttd()
+{
+ const char fn[] = "recup_dir.1/f0000000.ttd";
+ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+// register_header_check_fasttxt(&file_stats);
+ if(header_check_ttd(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_ttd; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.data_check == &data_check_ttd; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_ttd; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_ttd(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_ttd(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_ttd(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_txt()
+{
+ const char fn[] = "recup_dir.1/f0000000.txt";
+ 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.extension == \null; */
+ /*@ 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_txt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_txt(&file_stats);
+#endif
+ /*@ assert file_recovery.extension == \null; */
+ if(header_check_txt(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ assert valid_read_string((char *)&fn); */
+ /*@ assert file_recovery_new.extension != \null; */
+ 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 valid_read_string((char *)file_recovery_new.extension); */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.data_check == \null || file_recovery_new.data_check == &data_check_html || file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_check == &file_check_emlx || file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.file_rename == \null || file_recovery_new.file_rename == &file_rename_html; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_txt; */
+ if(file_recovery_new.data_check != NULL)
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_html || file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.extension); */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_txt(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_emlx || file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_recovery_new.file_check(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ if(file_recovery_new.file_rename != NULL)
+ {
+ /*@ assert file_recovery_new.file_rename == &file_rename_html; */
+ file_rename_html(&file_recovery_new);
+ }
+ return 0;
+}
+
+static int main_vbm()
+{
+ const char fn[] = "recup_dir.1/f0000000.vbm";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_vbm(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_vbm; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_vbm; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_vbm(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_vbm; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_vbm(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_xml()
+{
+ const char fn[] = "recup_dir.1/f0000000.xml";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_xml(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_gpx ||
+ file_recovery_new.file_check == &file_check_svg ||
+ file_recovery_new.file_check == &file_check_xml; */
+ /*@ assert file_recovery_new.data_check == \null ||
+ file_recovery_new.data_check == &data_check_html ||
+ file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_rename == \null ||
+ file_recovery_new.file_rename == &file_rename_fods ||
+ file_recovery_new.file_rename == &file_rename_html;
+ */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ if(file_recovery_new.data_check != NULL)
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_xml(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ if(file_recovery_new.file_check != NULL)
+ {
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_recovery_new.file_check(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ if(file_recovery_new.file_rename!=NULL)
+ {
+ file_recovery_new.file_rename(&file_recovery_new);
+ }
+ return 0;
+}
+
+static int main_xml_utf8()
+{
+ const char fn[] = "recup_dir.1/f0000000.xml";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_xml_utf8(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_ghx || file_recovery_new.extension == extension_xml; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_xml; */
+ /*@ assert file_recovery_new.data_check == &data_check_xml_utf8; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_xml_utf8; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_xml_utf8(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_xml_utf8(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.file_check == &file_check_xml; */
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_xml(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+static int main_xml_utf16()
+{
+ const char fn[] = "recup_dir.1/f0000000.xml";
+ 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.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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_xml_utf16(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_xml; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == \null; */
+ /*@ assert file_recovery_new.data_check == \null; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_xml_utf16(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert file_recovery_new.file_check == \null; */
+ return 0;
+}
+
+static int main_xmp()
+{
+ const char fn[] = "recup_dir.1/f0000000.xmp";
+ 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_fasttxt;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+#if 0
+ register_header_check_fasttxt(&file_stats);
+#endif
+ if(header_check_xmp(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ /*@ 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.extension == extension_xmp; */
+ /*@ assert file_recovery_new.calculated_file_size == 0; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_stat->file_hint==&file_hint_fasttxt; */
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ /*@ assert file_recovery_new.data_check == &data_check_txt; */
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ data_check_txt(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ header_check_xmp(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ /*@ assert valid_read_string((char *)file_recovery_new.filename); */
+ file_recovery_new.handle=fopen(fn, "rb");
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ if(file_recovery_new.handle!=NULL)
+ {
+ file_check_size(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ return 0;
+}
+
+int main()
+{
+ main_dc();
+ main_ers();
+ main_fasttxt();
+ main_html();
+ main_ics();
+ main_mbox();
+ main_perlm();
+ main_rtf();
+ main_smail();
+ main_snz();
+ main_stl();
+ main_svg();
+ main_thunderbird();
+ main_ttd();
+ main_txt();
+ main_vbm();
+ main_xml();
+ main_xml_utf8();
+ main_xml_utf16();
+ main_xmp();
+ return 0;
+}
+#endif