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

src/file_wld.c: add Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-03-14 13:23:05 +01:00
parent 74a9277425
commit d7ae24a472
1 changed files with 40 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
src/file_wld.c
View file

@ -32,54 +32,67 @@
#include "filegen.h"
#include "common.h"
/*@ requires \valid(file_stat); */
static void register_header_check_wld(file_stat_t *file_stat);
const file_hint_t file_hint_wld= {
.extension="wld",
.description="Terraria world",
.max_filesize=PHOTOREC_MAX_FILE_SIZE,
.recover=1,
.enable_by_default=1,
.register_header_check=&register_header_check_wld
const file_hint_t file_hint_wld = {
.extension = "wld",
.description = "Terraria world",
.max_filesize = PHOTOREC_MAX_FILE_SIZE,
.recover = 1,
.enable_by_default = 1,
.register_header_check = &register_header_check_wld
};
/* See http://ludwig.schafer.free.fr for WLD file format */
/*@
@ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ requires file_recovery->file_rename==&file_rename_wld;
@*/
static void file_rename_wld(file_recovery_t *file_recovery)
{
uint32_t offset;
unsigned char buffer[256];
FILE *file;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
if((file = fopen(file_recovery->filename, "rb")) == NULL)
return;
if (fseek(file, 0x1a, SEEK_SET) == -1 ||
fread(&offset, 4, 1, file)!=1 ||
fseek(file, le32(offset), SEEK_SET) == -1 ||
fread(&buffer, 256, 1, file)!=1)
if(fseek(file, 0x1a, SEEK_SET) == -1 || fread(&offset, 4, 1, file) != 1 || fseek(file, le32(offset), SEEK_SET) == -1 || fread(&buffer, 256, 1, file) != 1)
{
fclose(file);
return ;
return;
}
fclose(file);
file_rename(file_recovery, &buffer[1], buffer[0], 0, NULL, 1);
}
/*@
@ 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_wld, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_wld(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[0xB]<=0 || buffer[0xB]>3)
if(buffer[0xB] <= 0 || buffer[0xB] > 3)
return 0;
reset_file_recovery(file_recovery_new);
switch(buffer[0xb])
{
case 0x01:
file_recovery_new->extension="map";
file_recovery_new->extension = "map";
break;
case 0x02:
file_recovery_new->extension=file_hint_wld.extension;
file_recovery_new->file_rename=&file_rename_wld;
file_recovery_new->extension = file_hint_wld.extension;
file_recovery_new->file_rename = &file_rename_wld;
break;
case 0x03:
file_recovery_new->extension="plr";
file_recovery_new->extension = "plr";
break;
}
return 1;
@ -87,9 +100,10 @@ static int header_check_wld(const unsigned char *buffer, const unsigned int buff
static void register_header_check_wld(file_stat_t *file_stat)
{
static const unsigned char wld_header[10]= {
static const unsigned char wld_header[10] = {
0x00, 0x00, 0x00,
'r' , 'e' , 'l' , 'o' , 'g' , 'i' , 'c' };
'r', 'e', 'l', 'o', 'g', 'i', 'c'
};
register_header_check(1, wld_header, sizeof(wld_header), &header_check_wld, file_stat);
}
#endif