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

file_asf.c, file_reg.c: add frama-c annotations

Browse source 
td_ntfs2utc(): fix error reported by frama-c
This commit is contained in:
Christophe Grenier 2021-02-13 16:28:41 +01:00
parent f68f009d5f
commit cb76665f1c
3 changed files with 64 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/common.c
View file

@ -199,6 +199,9 @@ unsigned int up2power(const unsigned int number)
void set_part_name(partition_t *partition, const char *src, const unsigned int max_size)
{
unsigned int i;
/*@
@ loop assigns i, partition->fsname[i];
@*/
for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
partition->fsname[i]=src[i];
partition->fsname[i]='\0';
@ -207,8 +210,14 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size)
{
unsigned int i;
/*@
@ loop assigns i, partition->fsname[i];
@*/
for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
partition->fsname[i]=src[i];
/*@
@ loop assigns i;
@*/
while(i>0 && src[i-1]==' ')
i--;
partition->fsname[i]='\0';
@ -270,8 +279,6 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
day = td_max(1, f_date & 0x1f) - 1;
/*@ assert 0 <= day <= 30; */
leap_day = (year + 3) / 4;
/*@ assert 0 <= leap_day <= 32; */
if (year > YEAR_2100) /* 2100 isn't leap year */
{
/*@ assert year > YEAR_2100; */
@ -283,6 +290,7 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
else
{
/*@ assert year <= YEAR_2100; */
leap_day = (year + 3) / 4;
/*@ assert 0 <= leap_day <= (YEAR_2100 + 3)/4; */
}
/*@ assert 0 <= leap_day < 32; */
@ -341,7 +349,9 @@ void set_secwest(void)
#define NTFS_TIME_OFFSET ((int64_t)(369 * 365 + 89) * 24 * 3600 * 10000000)
time_t td_ntfs2utc (int64_t ntfstime)
{
return (ntfstime - (NTFS_TIME_OFFSET)) / 10000000;
if(ntfstime < NTFS_TIME_OFFSET)
return 0;
return (ntfstime - NTFS_TIME_OFFSET) / 10000000;
}
int check_command(char **current_cmd, const char *cmd, const size_t n)
@ -349,7 +359,17 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
const int res=strncmp(*current_cmd, cmd, n);
if(res==0)
{
#ifdef __FRAMAC__
unsigned int i;
/*@
@ loop invariant valid_read_string(*current_cmd);
@ loop assigns i, *current_cmd;
@*/
for(i=0; i<n && *current_cmd!='\0'; i++)
(*current_cmd)++;
#else
(*current_cmd)+=n;
#endif
/*@ assert valid_read_string(*current_cmd); */
return 0;
}

23
src/file_asf.c
View file

@ -33,8 +33,8 @@
#include "log.h"
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_asf)
/*@ requires \valid(file_stat); */
static void register_header_check_asf(file_stat_t *file_stat);
static int header_check_asf(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 file_hint_t file_hint_asf= {
.extension="asf",
@ -58,7 +58,7 @@ struct asf_file_prop_s {
uint64_t object_size;
unsigned char file_id[16];
uint64_t file_size;
uint64_t file_date;
int64_t file_date;
} __attribute__ ((gcc_struct, __packed__));
struct asf_stream_prop_s {
@ -70,6 +70,16 @@ struct asf_stream_prop_s {
static const char *extension_wma="wma";
static const char *extension_wmv="wmv";
/*@
@ requires buffer_size > sizeof(struct asf_header_obj_s);
@ 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_asf, buffer+(..), file_recovery, file_recovery_new);
@ assigns *file_recovery_new;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/
static int header_check_asf(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 asf_header_obj_s *hdr=(const struct asf_header_obj_s*)buffer;
@ -84,6 +94,9 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
le64(hdr->object_size) >= PHOTOREC_MAX_FILE_SIZE ||
nbr_header_obj<4)
return 0;
/*@
@ loop assigns extension, i, size, time, offset_prop;
@*/
for(i=0;
i < nbr_header_obj && offset_prop + 0x28 < buffer_size;
i++)
@ -102,7 +115,9 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
};
if(object_size < 0x18)
{
#ifndef __FRAMAC__
log_info("header_check_asf object_size too small %llu\n", (long long unsigned)object_size);
#endif
return 0;
}
if(object_size > 0x8000000000000000)
@ -119,10 +134,10 @@ static int header_check_asf(const unsigned char *buffer, const unsigned int buff
else if(memcmp(prop->object_id, asf_stream_prop_s, sizeof(asf_stream_prop_s))==0)
{
const struct asf_stream_prop_s *stream=(const struct asf_stream_prop_s *)prop;
const char wma[16]={
const unsigned char wma[16]={
0x40, 0x9e, 0x69, 0xf8, 0x4d, 0x5b, 0xcf, 0x11, 0xa8, 0xfd, 0x00, 0x80, 0x5f, 0x5c, 0x44, 0x2b
};
const char wmv[16]={
const unsigned char wmv[16]={
0xc0, 0xef, 0x19, 0xbc, 0x4d, 0x5b, 0xcf, 0x11, 0xa8, 0xfd, 0x00, 0x80, 0x5f, 0x5c, 0x44, 0x2b
};
if(object_size < 0x28)

23
src/file_reg.c
View file

@ -32,6 +32,7 @@
#include "common.h"
#include "filegen.h"
/*@ requires \valid(file_stat); */
static void register_header_check_reg(file_stat_t *file_stat);
const file_hint_t file_hint_reg= {
@ -70,6 +71,16 @@ struct rgdb_block
uint32_t chksum;
} __attribute__ ((gcc_struct, __packed__));
/*@
@ requires buffer_size > sizeof(struct creg_file_header);
@ 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_reg, buffer+(..), file_recovery, file_recovery_new);
@ assigns *file_recovery_new;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/
static int header_check_reg_9x(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 creg_file_header*header=(const struct creg_file_header*)buffer;
@ -91,7 +102,7 @@ struct regf_file_header
uint32_t signature;
uint32_t primary_sequence_number;
uint32_t secondary_sequence_number;
uint64_t modification_time;
int64_t modification_time;
uint32_t major_version;
uint32_t minor_version;
uint32_t file_type;
@ -104,6 +115,16 @@ struct regf_file_header
uint32_t xor_checksum;
} __attribute__ ((gcc_struct, __packed__));
/*@
@ requires buffer_size > sizeof(struct regf_file_header);
@ 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_reg, buffer+(..), file_recovery, file_recovery_new);
@ assigns *file_recovery_new;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
@*/
static int header_check_reg_nt(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 regf_file_header *header=(const struct regf_file_header*)buffer;