summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-01 16:34:38 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-01 16:34:38 +0100
commit611da961b33b7d1d0b68a8d7f87437417055dab5 (patch)
treedacb63b764eb983bb828d7e3eb8aca788784aec2 /src
parentf5f3120cfa5c60f8921a1244accf8026e0f1cd8c (diff)
add a few frama-c annotations
Diffstat (limited to 'src')
-rw-r--r--src/file_mov.c1
-rw-r--r--src/file_zip.c14
-rw-r--r--src/filegen.h3
3 files changed, 17 insertions, 1 deletions
diff --git a/src/file_mov.c b/src/file_mov.c
index 2246cd7..b330395 100644
--- a/src/file_mov.c
+++ b/src/file_mov.c
@@ -103,6 +103,7 @@ static void file_rename_mov(file_recovery_t *file_recovery)
/*@
@ requires buffer_size >= 16;
+ @ requires (buffer_size&1)==0;
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check==&data_check_mov;
diff --git a/src/file_zip.c b/src/file_zip.c
index 50578d9..c674b2f 100644
--- a/src/file_zip.c
+++ b/src/file_zip.c
@@ -852,22 +852,29 @@ static void file_check_zip(file_recovery_t *fr)
@ requires valid_read_string((char*)file_recovery->filename);
@ requires file_recovery->file_rename==&file_rename_zip;
@*/
+/* TODO ensures valid_read_string((char*)file_recovery->filename); */
static void file_rename_zip(file_recovery_t *file_recovery)
{
const char *ext=NULL;
unsigned int file_nbr=0;
file_recovery_t fr;
reset_file_recovery(&fr);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
if((fr.handle=fopen(file_recovery->filename, "rb"))==NULL)
+ {
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
+ }
fr.file_size = 0;
fr.offset_error=0;
first_filename[0]='\0';
if(my_fseek(fr.handle, 0, SEEK_SET) < 0)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return ;
}
+ /*@ loop invariant valid_read_string((char*)file_recovery->filename); */
while (1)
{
uint32_t header;
@@ -875,6 +882,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if(file_nbr>=0xffffffff || fr.file_size >= 0x8000000000000000 - 4)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
/*@ assert fr.file_size < 0x8000000000000000 - 4; */
@@ -885,6 +893,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
log_trace("Failed to read block header\n");
#endif
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
#if defined(__FRAMAC__)
@@ -921,7 +930,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if(ext!=NULL)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, NULL, 0, 0, ext, 1);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
break;
@@ -943,6 +954,7 @@ static void file_rename_zip(file_recovery_t *file_recovery)
if (status<0)
{
fclose(fr.handle);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
/* Only end of central dir is end of archive, 64b version of it is before */
@@ -956,7 +968,9 @@ static void file_rename_zip(file_recovery_t *file_recovery)
first_filename[len]!='/' &&
first_filename[len]!='\\';
len++);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
file_rename(file_recovery, first_filename, len, 0, "zip", 0);
+ /*@ assert valid_read_string((char*)file_recovery->filename); */
return;
}
}
diff --git a/src/filegen.h b/src/filegen.h
index 7a1807b..a7ebde4 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -144,7 +144,8 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
/*@
- @ requires buffer_size > 0;
+ @ requires buffer_size >= 2;
+ @ requires (buffer_size&1)==0;
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
@ requires file_recovery->data_check == &data_check_size;