summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-28 12:06:34 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-28 12:06:34 +0100
commit16882c98ea152cf344104e9e43a9b017a59819e3 (patch)
tree123f9378bbe818df55f4b26b65932e67974806ed
parentd00003e6e93e82fe4d7e279130e57595dbea2bc5 (diff)
date_dos2unix(): adapt a more recent and readable version from Linux kernel.
file_rsearch(): rewrite it add frama-c annotations to various functions
-rw-r--r--src/common.c48
-rw-r--r--src/common.h2
-rw-r--r--src/fidentify.c3
-rw-r--r--src/filegen.c30
-rw-r--r--src/filegen.h8
5 files changed, 63 insertions, 28 deletions
diff --git a/src/common.c b/src/common.c
index afcf387..8e9e7de 100644
--- a/src/common.c
+++ b/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;
}
diff --git a/src/common.h b/src/common.h
index 8a5e5ea..a7361fd 100644
--- a/src/common.h
+++ b/src/common.h
@@ -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);
diff --git a/src/fidentify.c b/src/fidentify.c
index 24b9544..be44e6b 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -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;
diff --git a/src/filegen.c b/src/filegen.c
index 1ad2270..93912c1 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -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 &&
diff --git a/src/filegen.h b/src/filegen.h
index a79d07a..7a1807b 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -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);