luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

src/file_r3d.c: add Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-04-10 11:04:41 +02:00
parent 2f01b7d825
commit cd787bb097
1 changed files with 105 additions and 66 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

171
src/file_r3d.c
View file

@ -34,119 +34,158 @@
#include "common.h" #include "common.h"
#include "log.h" #include "log.h"
/*@ requires \valid(file_stat); */
static void register_header_check_r3d(file_stat_t *file_stat); static void register_header_check_r3d(file_stat_t *file_stat);
static int header_check_r3d(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new);
static void file_rename_r3d(file_recovery_t *file_recovery);
const file_hint_t file_hint_r3d= { const file_hint_t file_hint_r3d = {
.extension="r3d", .extension = "r3d",
.description="RED r3d camera", .description = "RED r3d camera",
.max_filesize=PHOTOREC_MAX_FILE_SIZE, .max_filesize = PHOTOREC_MAX_FILE_SIZE,
.recover=1, .recover = 1,
.enable_by_default=1, .enable_by_default = 1,
.register_header_check=&register_header_check_r3d .register_header_check = &register_header_check_r3d
}; };
static const unsigned char r3d_header1[4]= { 'R' , 'E' , 'D' , '1' };
static const unsigned char r3d_header2[4]= { 'R' , 'E' , 'D' , '2' };
struct atom_struct struct atom_struct
{ {
uint32_t size; uint32_t size;
uint32_t type; uint32_t type;
} __attribute__ ((gcc_struct, __packed__)); } __attribute__((gcc_struct, __packed__));
/*@
@ requires buffer_size > 0;
@ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_r3d;
@ requires \separated(buffer + (..), file_recovery);
@ ensures \result == DC_CONTINUE || \result == DC_STOP;
@ assigns file_recovery->calculated_file_size, file_recovery->data_check;
@*/
static data_check_t data_check_r3d(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery) static data_check_t data_check_r3d(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{ {
while(file_recovery->calculated_file_size + buffer_size/2 >= file_recovery->file_size && /*@
file_recovery->calculated_file_size + 8 <= file_recovery->file_size + buffer_size/2) @ loop assigns file_recovery->calculated_file_size;
@*/
while(file_recovery->calculated_file_size + buffer_size / 2 >= file_recovery->file_size && file_recovery->calculated_file_size + 8 <= file_recovery->file_size + buffer_size / 2)
{ {
const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2; const unsigned int i = file_recovery->calculated_file_size + buffer_size / 2 - file_recovery->file_size;
const struct atom_struct *atom=(const struct atom_struct*)&buffer[i]; /*@ assert 0 <= i <= buffer_size-8; */
uint64_t atom_size=be32(atom->size); const struct atom_struct *atom = (const struct atom_struct *)&buffer[i];
if(atom_size<8) uint64_t atom_size = be32(atom->size);
if(atom_size < 8)
return DC_STOP; return DC_STOP;
#ifdef DEBUG_R3D #ifdef DEBUG_R3D
log_trace("file_r3d.c: %s atom %c%c%c%c (0x%02x%02x%02x%02x) size %llu, calculated_file_size %llu\n", log_trace("file_r3d.c: %s atom %c%c%c%c (0x%02x%02x%02x%02x) size %llu, calculated_file_size %llu\n",
file_recovery->filename, file_recovery->filename,
buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7], buffer[i + 4], buffer[i + 5], buffer[i + 6], buffer[i + 7],
buffer[i+4],buffer[i+5],buffer[i+6],buffer[i+7], buffer[i + 4], buffer[i + 5], buffer[i + 6], buffer[i + 7],
(long long unsigned)atom_size, (long long unsigned)atom_size,
(long long unsigned)file_recovery->calculated_file_size); (long long unsigned)file_recovery->calculated_file_size);
#endif #endif
if(buffer[i+4]=='R' && buffer[i+5]=='E' && buffer[i+6]=='O') if(buffer[i + 4] == 'R' && buffer[i + 5] == 'E' && buffer[i + 6] == 'O')
{ {
/* End of file */ /* End of file */
file_recovery->calculated_file_size+=atom_size; file_recovery->calculated_file_size += atom_size;
file_recovery->data_check=NULL; file_recovery->data_check = NULL;
return DC_CONTINUE; return DC_CONTINUE;
} }
if(buffer[i+4]!='R') if(buffer[i + 4] != 'R')
{ {
return DC_STOP; return DC_STOP;
} }
/* REDV1 REDV RPAD RDVO RDVS RDAO RDAS REOB */ /* REDV1 REDV RPAD RDVO RDVS RDAO RDAS REOB */
file_recovery->calculated_file_size+=atom_size; file_recovery->calculated_file_size += atom_size;
} }
#ifdef DEBUG_R3D #ifdef DEBUG_R3D
log_trace("file_r3d.c: new calculated_file_size %llu\n", log_trace("file_r3d.c: new calculated_file_size %llu\n",
(long long unsigned)file_recovery->calculated_file_size); (long long unsigned)file_recovery->calculated_file_size);
#endif #endif
return DC_CONTINUE; return DC_CONTINUE;
} }
static int header_check_r3d(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);
const struct atom_struct *atom=(const struct atom_struct*)buffer; @ requires valid_file_recovery(file_recovery);
if(be32(atom->size) < 8) @ requires file_recovery->file_rename==&file_rename_r3d;
return 0; @*/
if(buffer[0xa]=='R' && buffer[0xb]=='1')
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_r3d.extension;
file_recovery_new->file_rename=&file_rename_r3d;
if(file_recovery_new->blocksize < 8)
return 1;
file_recovery_new->data_check=&data_check_r3d;
file_recovery_new->file_check=&file_check_size;
return 1;
}
return 0;
}
static int header_check_r3d_v2(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[0xa]=='R' && buffer[0xb]=='2')
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_r3d.extension;
return 1;
}
return 0;
}
static void file_rename_r3d(file_recovery_t *file_recovery) static void file_rename_r3d(file_recovery_t *file_recovery)
{ {
unsigned char buffer[512]; unsigned char buffer[512];
FILE *file; FILE *file;
size_t buffer_size; size_t buffer_size;
unsigned int i; unsigned int i;
if((file=fopen(file_recovery->filename, "rb"))==NULL) if((file = fopen(file_recovery->filename, "rb")) == NULL)
return; return;
buffer_size=fread(buffer, 1, sizeof(buffer), file); buffer_size = fread(buffer, 1, sizeof(buffer), file);
fclose(file); fclose(file);
if(buffer_size<0x44) if(buffer_size < 0x44)
return; return;
for(i=0x43; i< buffer_size && buffer[i]!=0 && buffer[i]!='.'; i++) /*@ loop assigns i; */
for(i = 0x43; i < buffer_size && buffer[i] != 0 && buffer[i] != '.'; i++)
{ {
if(!isalnum(buffer[i]) && buffer[i]!='_') if(!isalnum(buffer[i]) && buffer[i] != '_')
return ; return;
} }
file_rename(file_recovery, buffer, i, 0x43, NULL, 1); file_rename(file_recovery, buffer, i, 0x43, NULL, 1);
} }
/*@
@ requires buffer_size >= sizeof(struct atom_struct);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_r3d, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_r3d(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 struct atom_struct *atom = (const struct atom_struct *)buffer;
if(be32(atom->size) < 8)
return 0;
if(buffer[0xa] == 'R' && buffer[0xb] == '1')
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension = file_hint_r3d.extension;
file_recovery_new->file_rename = &file_rename_r3d;
if(file_recovery_new->blocksize < 8)
return 1;
file_recovery_new->data_check = &data_check_r3d;
file_recovery_new->file_check = &file_check_size;
return 1;
}
return 0;
}
/*@
@ requires buffer_size >= 0xc;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_r3d, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_r3d_v2(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[0xa] == 'R' && buffer[0xb] == '2')
{
reset_file_recovery(file_recovery_new);
file_recovery_new->extension = file_hint_r3d.extension;
return 1;
}
return 0;
}
static void register_header_check_r3d(file_stat_t *file_stat) static void register_header_check_r3d(file_stat_t *file_stat)
{ {
static const unsigned char r3d_header1[4] = { 'R', 'E', 'D', '1' };
static const unsigned char r3d_header2[4] = { 'R', 'E', 'D', '2' };
register_header_check(4, r3d_header1, sizeof(r3d_header1), &header_check_r3d, file_stat); register_header_check(4, r3d_header1, sizeof(r3d_header1), &header_check_r3d, file_stat);
register_header_check(4, r3d_header2, sizeof(r3d_header2), &header_check_r3d_v2, file_stat); register_header_check(4, r3d_header2, sizeof(r3d_header2), &header_check_r3d_v2, file_stat);
} }