summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:12:22 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:12:22 +0200
commita43423c2badcc38c3843556558706d26601d7cfe (patch)
tree52d0d424ba13dddfd601ef5361193adc3c9a47c7
parent823fd459972beb02bc4148461247a01dc010a006 (diff)
Make file_check_cmp() frama-c friendly
Disable file_rename() and file_rename_unicode_aux() when parsed by frama-c
-rw-r--r--src/filegen.c8
-rw-r--r--src/filegen.h2
2 files changed, 8 insertions, 2 deletions
diff --git a/src/filegen.c b/src/filegen.c
index 800727c..dc12987 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -65,7 +65,7 @@ static int file_check_cmp(const struct td_list_head *a, const struct td_list_hea
res=memcmp(fc_a->value,fc_b->value, (fc_a->length<=fc_b->length?fc_a->length:fc_b->length));
if(res!=0)
return res;
- return fc_b->length-fc_a->length;
+ return (int)fc_b->length-(int)fc_a->length;
}
static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t *pos)
@@ -439,6 +439,8 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext,
/* 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)
{
+ /* TODO: make the code from frama-c friendly */
+#ifndef __FRAMAC__
/* new_filename is large enough to avoid a buffer overflow */
char *new_filename;
const char *src=file_recovery->filename;
@@ -550,6 +552,7 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
strcpy(file_recovery->filename, new_filename);
}
free(new_filename);
+#endif
return 0;
}
@@ -609,6 +612,8 @@ static int file_rename_unicode_aux(file_recovery_t *file_recovery, const char *n
/* The original filename begins at offset in buffer and is null terminated */
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)
{
+ /* TODO: make the code from frama-c friendly */
+#ifndef __FRAMAC__
/* new_filename is large enough to avoid a buffer overflow */
char *new_filename;
const char *src=file_recovery->filename;
@@ -713,6 +718,7 @@ int file_rename_unicode(file_recovery_t *file_recovery, const void *buffer, cons
strcpy(file_recovery->filename, new_filename);
}
free(new_filename);
+#endif
return 0;
}
diff --git a/src/filegen.h b/src/filegen.h
index 2436fc6..1e2fb4e 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -211,7 +211,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
void reset_file_recovery(file_recovery_t *file_recovery);
/*@
- @ requires length > 0;
+ @ requires 0 < length <= 4096;
@ requires \valid_read((char *)value+(0..length-1));
@ requires \valid_function(header_check);
@ requires \valid(file_stat);