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

src/file_gz.c: improve Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-06-15 17:18:55 +02:00
parent 9ec38fdbc1
commit 71c00808f7
1 changed files with 43 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
src/file_gz.c
View file

@ -43,9 +43,8 @@
#include "filegen.h"
#include "common.h"
/*@ requires \valid(file_stat); */
/*@ requires valid_register_header_check(file_stat); */
static void register_header_check_gz(file_stat_t *file_stat);
static void file_rename_gz(file_recovery_t *file_recovery);
#ifndef SINGLE_FORMAT
extern const file_hint_t file_hint_doc;
#endif
@ -85,6 +84,43 @@ struct gzip_header
#define GZ_FNAME 8
#define GZ_FCOMMENT 0x10
/*@
@ requires file_recovery->file_rename==&file_rename_gz;
@ requires valid_file_rename_param(file_recovery);
@ ensures valid_file_rename_result(file_recovery);
@*/
static void file_rename_gz(file_recovery_t *file_recovery)
{
unsigned char buffer[512];
FILE *file;
int buffer_size;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
return;
buffer_size=fread(buffer, 1, sizeof(buffer), file);
fclose(file);
if(buffer_size<10)
return;
/*@ assert \initialized(buffer+(0..10)); */
if(!(buffer[0]==0x1F && buffer[1]==0x8B && buffer[2]==0x08 && (buffer[3]&0xe0)==0))
return ;
{
const unsigned int flags=buffer[3];
int off=10;
if((flags&GZ_FEXTRA)!=0)
{
if(buffer_size<12)
return;
/*@ assert \initialized(buffer + (0 .. 12)); */
off+=2;
off+=buffer[10]|(buffer[11]<<8);
}
if((flags&GZ_FNAME)!=0)
{
file_rename(file_recovery, buffer, buffer_size, off, NULL, 1);
}
}
}
#if defined(HAVE_ZLIB_H) && defined(HAVE_LIBZ)
/*@ assigns \nothing; */
static void file_check_bgzf(file_recovery_t *file_recovery)
@ -97,9 +133,10 @@ static void file_check_bgzf(file_recovery_t *file_recovery)
@ requires \valid_read(buffer_uncompr + (0 .. 4-1));
@ requires \valid(file_recovery_new);
@ requires separation: \separated(buffer+(..), file_recovery_new);
@ assigns *file_recovery_new;
@ requires valid_file_recovery(file_recovery_new);
@ ensures \result == 1;
@ ensures valid_file_recovery(file_recovery_new);
@ ensures valid_header_check_result(\result, file_recovery_new);
@ assigns *file_recovery_new;
@*/
static int header_check_bgzf(const unsigned char *buffer, const unsigned char *buffer_uncompr, const unsigned int buffer_size, file_recovery_t *file_recovery_new)
{
@ -138,13 +175,9 @@ static int header_check_bgzf(const unsigned char *buffer, const unsigned char *b
/*@
@ requires buffer_size >= 16;
@ 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_gz, buffer+(..), file_recovery, file_recovery_new);
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures valid_header_check_result(\result, file_recovery_new);
@*/
static int header_check_gz(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)
{
@ -369,39 +402,6 @@ static int header_check_gz(const unsigned char *buffer, const unsigned int buffe
return 1;
}
/*@
@ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ requires file_recovery->file_rename==&file_rename_gz;
@*/
static void file_rename_gz(file_recovery_t *file_recovery)
{
unsigned char buffer[512];
FILE *file;
int buffer_size;
if((file=fopen(file_recovery->filename, "rb"))==NULL)
return;
buffer_size=fread(buffer, 1, sizeof(buffer), file);
fclose(file);
if(buffer_size<10)
return;
if(!(buffer[0]==0x1F && buffer[1]==0x8B && buffer[2]==0x08 && (buffer[3]&0xe0)==0))
return ;
{
const unsigned int flags=buffer[3];
int off=10;
if((flags&GZ_FEXTRA)!=0)
{
off+=2;
off+=buffer[10]|(buffer[11]<<8);
}
if((flags&GZ_FNAME)!=0)
{
file_rename(file_recovery, buffer, buffer_size, off, NULL, 1);
}
}
}
static void register_header_check_gz(file_stat_t *file_stat)
{
static const unsigned char gz_header_magic[3]= {0x1F, 0x8B, 0x08};