src/file_indd.c: fix Frama-C warnings
This commit is contained in:
parent
13eb09f44e
commit
e677eb6b6a
1 changed files with 12 additions and 21 deletions
|
@ -34,10 +34,8 @@
|
||||||
#include "filegen.h"
|
#include "filegen.h"
|
||||||
#include "log.h"
|
#include "log.h"
|
||||||
|
|
||||||
/*@ requires \valid(file_stat); */
|
/*@ requires valid_register_header_check(file_stat); */
|
||||||
static void register_header_check_indd(file_stat_t *file_stat);
|
static void register_header_check_indd(file_stat_t *file_stat);
|
||||||
static int header_check_indd(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new);
|
|
||||||
static void file_check_indd(file_recovery_t *file_recovery);
|
|
||||||
|
|
||||||
const file_hint_t file_hint_indd= {
|
const file_hint_t file_hint_indd= {
|
||||||
.extension="indd",
|
.extension="indd",
|
||||||
|
@ -76,16 +74,12 @@ struct InDesignContigObjMarker {
|
||||||
} __attribute__ ((gcc_struct, __packed__));
|
} __attribute__ ((gcc_struct, __packed__));
|
||||||
|
|
||||||
/*@
|
/*@
|
||||||
@ requires valid_file_recovery(file_recovery);
|
|
||||||
@ requires \valid(file_recovery->handle);
|
|
||||||
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
|
|
||||||
@ requires \initialized(&file_recovery->time);
|
|
||||||
@
|
|
||||||
@ requires file_recovery->file_check == &file_check_indd;
|
@ requires file_recovery->file_check == &file_check_indd;
|
||||||
|
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
|
||||||
|
@ requires valid_file_check_param(file_recovery);
|
||||||
|
@ ensures valid_file_check_result(file_recovery);
|
||||||
@ assigns *file_recovery->handle, errno, file_recovery->file_size;
|
@ assigns *file_recovery->handle, errno, file_recovery->file_size;
|
||||||
@ assigns Frama_C_entropy_source;
|
@ assigns Frama_C_entropy_source;
|
||||||
@
|
|
||||||
@ ensures \valid(file_recovery->handle);
|
|
||||||
@*/
|
@*/
|
||||||
static void file_check_indd(file_recovery_t *file_recovery)
|
static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
{
|
{
|
||||||
|
@ -104,7 +98,8 @@ static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
@*/
|
@*/
|
||||||
do
|
do
|
||||||
{
|
{
|
||||||
struct InDesignContigObjMarker hdr;
|
char buffer[sizeof(struct InDesignContigObjMarker)];
|
||||||
|
const struct InDesignContigObjMarker *hdr=(const struct InDesignContigObjMarker *)&buffer;;
|
||||||
#ifdef DEBUG_INDD
|
#ifdef DEBUG_INDD
|
||||||
log_info("file_check_indd offset=%llu (0x%llx)\n", (long long unsigned)offset, (long long unsigned)offset);
|
log_info("file_check_indd offset=%llu (0x%llx)\n", (long long unsigned)offset, (long long unsigned)offset);
|
||||||
#endif
|
#endif
|
||||||
|
@ -113,7 +108,7 @@ static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
file_recovery->file_size=0;
|
file_recovery->file_size=0;
|
||||||
return ;
|
return ;
|
||||||
}
|
}
|
||||||
if(fread(&hdr, sizeof(hdr), 1, file_recovery->handle) != 1)
|
if(fread(buffer, sizeof(buffer), 1, file_recovery->handle) != 1)
|
||||||
{
|
{
|
||||||
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
||||||
if(file_recovery->file_size>file_size_org)
|
if(file_recovery->file_size>file_size_org)
|
||||||
|
@ -121,9 +116,9 @@ static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
return ;
|
return ;
|
||||||
}
|
}
|
||||||
#ifdef __FRAMAC__
|
#ifdef __FRAMAC__
|
||||||
Frama_C_make_unknown(&hdr, sizeof(hdr));
|
Frama_C_make_unknown(buffer, sizeof(buffer));
|
||||||
#endif
|
#endif
|
||||||
if(memcmp(hdr.fGUID, kINDDContigObjHeaderGUID, sizeof(kINDDContigObjHeaderGUID))!=0)
|
if(memcmp(hdr->fGUID, kINDDContigObjHeaderGUID, sizeof(kINDDContigObjHeaderGUID))!=0)
|
||||||
{
|
{
|
||||||
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
||||||
if(file_recovery->file_size>file_size_org)
|
if(file_recovery->file_size>file_size_org)
|
||||||
|
@ -131,7 +126,7 @@ static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
return ;
|
return ;
|
||||||
}
|
}
|
||||||
/* header + data + trailer */
|
/* header + data + trailer */
|
||||||
offset+=(uint64_t)le32(hdr.fStreamLength)+2*sizeof(struct InDesignContigObjMarker);
|
offset+=(uint64_t)le32(hdr->fStreamLength)+2*sizeof(struct InDesignContigObjMarker);
|
||||||
} while(offset < file_size_org);
|
} while(offset < file_size_org);
|
||||||
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
file_recovery->file_size=(offset+4096-1)/4096*4096;
|
||||||
if(file_recovery->file_size>file_size_org)
|
if(file_recovery->file_size>file_size_org)
|
||||||
|
@ -141,13 +136,9 @@ static void file_check_indd(file_recovery_t *file_recovery)
|
||||||
|
|
||||||
/*@
|
/*@
|
||||||
@ requires buffer_size >= 4096 + sizeof(struct InDesignMasterPage);
|
@ requires buffer_size >= 4096 + sizeof(struct InDesignMasterPage);
|
||||||
@ 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_indd, buffer+(..), file_recovery, file_recovery_new);
|
@ requires separation: \separated(&file_hint_indd, buffer+(..), file_recovery, file_recovery_new);
|
||||||
@ ensures \result == 0 || \result == 1;
|
@ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
|
||||||
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
|
@ ensures valid_header_check_result(\result, file_recovery_new);
|
||||||
@*/
|
@*/
|
||||||
static int header_check_indd(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 int header_check_indd(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)
|
||||||
{
|
{
|
||||||
|
|
Loading…
Reference in a new issue