date_dos2unix(): adapt a more recent and readable version from Linux kernel.
file_rsearch(): rewrite it add frama-c annotations to various functions
This commit is contained in:
Christophe Grenier
parent
d00003e6e9
commit
16882c98ea
5 changed files with 63 additions and 28 deletions
48
src/common.c
48
src/common.c
|
|
@ -225,22 +225,50 @@ char* strip_dup(char* str)
|
|||
}
|
||||
|
||||
/* Convert a MS-DOS time/date pair to a UNIX date (seconds since 1 1 70). */
|
||||
/*
|
||||
* The epoch of FAT timestamp is 1980.
|
||||
* : bits : value
|
||||
* date: 0 - 4: day (1 - 31)
|
||||
* date: 5 - 8: month (1 - 12)
|
||||
* date: 9 - 15: year (0 - 127) from 1980
|
||||
* time: 0 - 4: sec (0 - 29) 2sec counts
|
||||
* time: 5 - 10: min (0 - 59)
|
||||
* time: 11 - 15: hour (0 - 23)
|
||||
*/
|
||||
#define SECS_PER_MIN 60
|
||||
#define SECS_PER_HOUR (60 * 60)
|
||||
#define SECS_PER_DAY (SECS_PER_HOUR * 24)
|
||||
/* days between 1.1.70 and 1.1.80 (2 leap days) */
|
||||
#define DAYS_DELTA (365 * 10 + 2)
|
||||
/* 120 (2100 - 1980) isn't leap year */
|
||||
#define YEAR_2100 120
|
||||
#define IS_LEAP_YEAR(y) (!((y) & 3) && (y) != YEAR_2100)
|
||||
|
||||
time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
|
||||
{
|
||||
static const unsigned int day_n[] = { 0,31,59,90,120,151,181,212,243,273,304,334,0,0,0,0 };
|
||||
static const unsigned int days_in_year[] = { 0, 0,31,59,90,120,151,181,212,243,273,304,334,0,0,0 };
|
||||
/* JanFebMarApr May Jun Jul Aug Sep Oct Nov Dec */
|
||||
|
||||
unsigned int month,year,secs;
|
||||
unsigned long int day,leap_day,month,year,days;
|
||||
unsigned long int secs;
|
||||
year = f_date >> 9;
|
||||
month = td_max(1, (f_date >> 5) & 0xf);
|
||||
day = td_max(1, f_date & 0x1f) - 1;
|
||||
|
||||
leap_day = (year + 3) / 4;
|
||||
if (year > YEAR_2100) /* 2100 isn't leap year */
|
||||
leap_day--;
|
||||
if (IS_LEAP_YEAR(year) && month > 2)
|
||||
leap_day++;
|
||||
days = days_in_year[month];
|
||||
/*@ assert days <= 334; */
|
||||
days += year * 365 + leap_day + day + DAYS_DELTA;
|
||||
|
||||
secs = (f_time & 0x1f)<<1;
|
||||
secs += ((f_time >> 5) & 0x3f) * SECS_PER_MIN;
|
||||
secs += (f_time >> 11)* SECS_PER_HOUR;
|
||||
secs += days * SECS_PER_DAY;
|
||||
|
||||
/* first subtract and mask after that... Otherwise, if
|
||||
f_date == 0, bad things happen */
|
||||
month = ((f_date >> 5) - 1) & 15;
|
||||
year = f_date >> 9;
|
||||
secs = (f_time & 31)*2+60*((f_time >> 5) & 63)+(f_time >> 11)*3600+86400*
|
||||
((f_date & 31)-1+day_n[month]+(year/4)+year*365-((year & 3) == 0 &&
|
||||
month < 2 ? 1 : 0)+3653);
|
||||
/* days since 1.1.70 plus 80's leap day */
|
||||
return secs+secwest;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -449,6 +449,8 @@ unsigned int up2power(const unsigned int number);
|
|||
void set_part_name(partition_t *partition, const char *src, const unsigned int max_size);
|
||||
void set_part_name_chomp(partition_t *partition, const unsigned char *src, const unsigned int max_size);
|
||||
char* strip_dup(char* str);
|
||||
|
||||
/*@ assigns \nothing; */
|
||||
time_t date_dos2unix(const unsigned short f_time,const unsigned short f_date);
|
||||
void set_secwest(void);
|
||||
time_t td_ntfs2utc (int64_t ntfstime);
|
||||
|
|
|
|||
|
|
@ -85,9 +85,10 @@ static int file_identify(const char *filename, const unsigned int options)
|
|||
file_recovery_t file_recovery_new;
|
||||
file_recovery_t file_recovery;
|
||||
reset_file_recovery(&file_recovery);
|
||||
reset_file_recovery(&file_recovery_new);
|
||||
file_recovery.blocksize=blocksize;
|
||||
file_recovery_new.blocksize=blocksize;
|
||||
file_recovery_new.file_stat=NULL;
|
||||
/*@ assert file_recovery_new.file_stat==NULL; */
|
||||
td_list_for_each(tmpl, &file_check_list.list)
|
||||
{
|
||||
struct td_list_head *tmp;
|
||||
|
|
|
|||
|
|
@ -235,14 +235,23 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
|
|||
{
|
||||
int i;
|
||||
int taille;
|
||||
const unsigned int read_size=(offset%4096!=0 ? offset%4096 : 4096);
|
||||
offset-=read_size;
|
||||
if(offset <= 4096)
|
||||
offset=0;
|
||||
else if(offset%4096==0)
|
||||
offset-=4096;
|
||||
else
|
||||
offset=offset-(offset%4096);
|
||||
if(my_fseek(handle,offset,SEEK_SET)<0)
|
||||
{
|
||||
free(buffer);
|
||||
return 0;
|
||||
}
|
||||
taille=fread(buffer, 1, read_size, handle);
|
||||
taille=fread(buffer, 1, 4096, handle);
|
||||
if(taille <= 0)
|
||||
{
|
||||
free(buffer);
|
||||
return 0;
|
||||
}
|
||||
for(i=taille-1;i>=0;i--)
|
||||
{
|
||||
if(buffer[i]==*(const unsigned char *)footer && memcmp(buffer+i,footer,footer_length)==0)
|
||||
|
|
@ -264,6 +273,7 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
|
|||
file_recovery->file_size=file_rsearch(file_recovery->handle, file_recovery->file_size-extra_length, footer, footer_length);
|
||||
if(file_recovery->file_size > 0)
|
||||
file_recovery->file_size+= footer_length + extra_length;
|
||||
/*@ assert \valid(file_recovery->handle); */
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
|
@ -577,13 +587,6 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
|
|||
return -1;
|
||||
}
|
||||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ ensures valid_read_string((char*)&file_recovery->filename);
|
||||
@*/
|
||||
/* The original filename begins at offset in buffer and is null terminated */
|
||||
int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
|
||||
{
|
||||
|
|
@ -707,13 +710,6 @@ static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buff
|
|||
return -1;
|
||||
}
|
||||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ ensures valid_read_string((char*)&file_recovery->filename);
|
||||
@*/
|
||||
int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int append_original_ext)
|
||||
{
|
||||
if(buffer!=NULL && 0 <= offset && offset < buffer_size &&
|
||||
|
|
|
|||
|
|
@ -123,6 +123,7 @@ void free_header_check(void);
|
|||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires \valid(file_recovery->handle);
|
||||
@ ensures \valid(file_recovery->handle);
|
||||
@*/
|
||||
void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);
|
||||
|
||||
|
|
@ -135,8 +136,10 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
|
|||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires \valid(file_recovery->handle);
|
||||
@ requires footer_length > 0;
|
||||
@ requires \valid_read((char *)footer+(0..footer_length-1));
|
||||
@ ensures \valid(file_recovery->handle);
|
||||
@*/
|
||||
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
|
||||
|
||||
|
|
@ -153,18 +156,21 @@ data_check_t data_check_size(const unsigned char *buffer, const unsigned int buf
|
|||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires file_recovery->file_check == &file_check_size;
|
||||
@ assigns file_recovery->file_size;
|
||||
@*/
|
||||
void file_check_size(file_recovery_t *file_recovery);
|
||||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires file_recovery->file_check == &file_check_size_min;
|
||||
@ assigns file_recovery->file_size;
|
||||
@*/
|
||||
void file_check_size_min(file_recovery_t *file_recovery);
|
||||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires file_recovery->file_check == &file_check_size_max;
|
||||
@ assigns file_recovery->file_size;
|
||||
@*/
|
||||
void file_check_size_max(file_recovery_t *file_recovery);
|
||||
|
||||
|
|
@ -236,6 +242,7 @@ file_stat_t * init_file_stats(file_enable_t *files_enable);
|
|||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ ensures valid_read_string((char*)&file_recovery->filename);
|
||||
@*/
|
||||
int file_rename(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
|
||||
|
||||
|
|
@ -244,6 +251,7 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
|
|||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ ensures valid_read_string((char*)&file_recovery->filename);
|
||||
@*/
|
||||
int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, const int buffer_size, const int offset, const char *new_ext, const int force_ext);
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue