summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:09:35 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:09:35 +0100
commite5f0da285517e25744a4b7284a64c16ddc75ed11 (patch)
treee8245fd57cae83eda682af10bc31293fe1f9bb30
parent8d120ade61d34732dd388de48222b6803ee8eda8 (diff)
add frama-c annotations for td_memmem() and several list related
functions
-rw-r--r--src/filegen.c35
-rw-r--r--src/filegen.h6
-rw-r--r--src/list.h33
-rw-r--r--src/memmem.h8
4 files changed, 80 insertions, 2 deletions
diff --git a/src/filegen.c b/src/filegen.c
index c197b5e..4862c93 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -39,6 +39,9 @@
#include "common.h"
#include "filegen.h"
#include "log.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static file_check_t file_check_plist={
.list = TD_LIST_HEAD_INIT(file_check_plist.list)
@@ -50,11 +53,18 @@ file_check_list_t file_check_list={
static unsigned int index_header_check(void);
+/*@
+ @ requires \valid_read(a);
+ @ requires \valid_read(b);
+ @*/
static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
{
const file_check_t *fc_a=td_list_entry_const(a, const file_check_t, list);
const file_check_t *fc_b=td_list_entry_const(b, const file_check_t, list);
int res;
+ unsigned int min_length;
+ /*@ assert \valid_read(fc_a); */
+ /*@ assert \valid_read(fc_b); */
if(fc_a->length==0 && fc_b->length!=0)
return -1;
if(fc_a->length!=0 && fc_b->length==0)
@@ -62,7 +72,14 @@ static int file_check_cmp(const struct td_list_head *a, const struct td_list_hea
res=fc_a->offset-fc_b->offset;
if(res!=0)
return res;
- res=memcmp(fc_a->value,fc_b->value, (fc_a->length<=fc_b->length?fc_a->length:fc_b->length));
+ /*@ assert \valid_read((char *)fc_a->value + (0 .. fc_a->length - 1)); */
+ /*@ assert \initialized((char *)fc_a->value + (0 .. fc_a->length - 1)); */
+#if 0
+ /*@ assert \valid_read((char *)fc_b->value + (0 .. fc_b->length - 1)); */
+ /*@ assert \initialized((char *)fc_b->value + (0 .. fc_b->length - 1)); */
+#endif
+ min_length=fc_a->length<=fc_b->length?fc_a->length:fc_b->length;
+ res=memcmp(fc_a->value,fc_b->value, min_length);
if(res!=0)
return res;
return (int)fc_b->length-(int)fc_a->length;
@@ -95,10 +112,15 @@ void register_header_check(const unsigned int offset, const void *value, const u
td_list_add_sorted(&file_check_new->list, &file_check_plist.list, file_check_cmp);
}
+/*@
+ @ requires \valid(file_check_new);
+ @*/
static void index_header_check_aux(file_check_t *file_check_new)
{
if(file_check_new->length>0)
{
+ /*@ assert file_check_new->offset < 0x80000000; */
+ /*@ assert 0 < file_check_new->length <= 4096; */
struct td_list_head *tmp;
td_list_for_each(tmp, &file_check_list.list)
{
@@ -186,6 +208,9 @@ void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode)
if(my_fseek(file_recovery->handle, file_recovery->file_size,SEEK_SET)<0)
return;
taille=fread(buffer,1, 4096,file_recovery->handle);
+#ifdef __FRAMAC__
+ Frama_C_make_unknown((char *)&buffer, 4096);
+#endif
if(taille > 0 && buffer[0]=='\n' && (nl_mode&NL_BARENL)==NL_BARENL)
file_recovery->file_size++;
else if(taille > 1 && buffer[0]=='\r' && buffer[1]=='\n' && (nl_mode&NL_CRLF)==NL_CRLF)
@@ -198,7 +223,13 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
{
unsigned char*buffer;
assert(footer_length < 4096);
- buffer=(unsigned char*)MALLOC(4096+footer_length-1);
+ /*@ assert 0 < footer_length < 4096; */
+ /*
+ * 4096+footer_length-1: required size
+ * 4096+footer_length: to avoid a Frama-C warning when footer_length==1
+ * 8192: maximum size
+ * */
+ buffer=(unsigned char*)MALLOC(4096+footer_length);
memset(buffer+4096,0,footer_length-1);
do
{
diff --git a/src/filegen.h b/src/filegen.h
index 31aabfa..a79d07a 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -122,6 +122,7 @@ void free_header_check(void);
/*@
@ requires \valid(file_recovery);
+ @ requires \valid(file_recovery->handle);
@*/
void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);
@@ -143,6 +144,7 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
@ requires buffer_size > 0;
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
@ requires \valid(file_recovery);
+ @ requires file_recovery->data_check == &data_check_size;
@ assigns \nothing;
@ ensures \result == DC_STOP || \result == DC_CONTINUE;
@*/
@@ -150,16 +152,19 @@ 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;
@*/
void file_check_size(file_recovery_t *file_recovery);
/*@
@ requires \valid(file_recovery);
+ @ requires file_recovery->file_check == &file_check_size_min;
@*/
void file_check_size_min(file_recovery_t *file_recovery);
/*@
@ requires \valid(file_recovery);
+ @ requires file_recovery->file_check == &file_check_size_max;
@*/
void file_check_size_max(file_recovery_t *file_recovery);
@@ -211,6 +216,7 @@ void file_check_size_max(file_recovery_t *file_recovery);
void reset_file_recovery(file_recovery_t *file_recovery);
/*@
+ @ requires offset < 0x80000000;
@ requires 0 < length <= 4096;
@ requires \valid_read((char *)value+(0..length-1));
@ requires \valid_function(header_check);
diff --git a/src/list.h b/src/list.h
index 29e8dad..2cd2995 100644
--- a/src/list.h
+++ b/src/list.h
@@ -59,6 +59,17 @@ struct td_list_head {
* This is only for internal list manipulation where we know
* the prev/next entries already!
*/
+/*@
+ @ requires \valid(newe);
+ @ requires \valid(prev);
+ @ requires \valid(next);
+ @ requires separation: \separated(newe, \union(prev,next));
+ @ ensures next->prev == newe;
+ @ ensures newe->next == next;
+ @ ensures newe->prev == prev;
+ @ ensures prev->next == newe;
+ @ assigns next->prev,newe->next,newe->prev,prev->next;
+ @*/
static inline void __td_list_add(struct td_list_head *newe,
struct td_list_head *prev,
struct td_list_head *next)
@@ -90,6 +101,16 @@ static inline void td_list_add(struct td_list_head *newe, struct td_list_head *h
* Insert a new entry before the specified head.
* This is useful for implementing queues.
*/
+/*@
+ @ requires \valid(newe);
+ @ requires \valid(head);
+ @ requires separation: \separated(newe, head);
+ @ ensures head->prev == newe;
+ @ ensures newe->next == head;
+ @ ensures newe->prev == \old(head->prev);
+ @ ensures \old(head->prev)->next == newe;
+ @ assigns head->prev,newe->next,newe->prev,\old(head->prev)->next;
+ @*/
static inline void td_list_add_tail(struct td_list_head *newe, struct td_list_head *head)
{
__td_list_add(newe, head->prev, head);
@@ -372,6 +393,12 @@ static inline void td_list_splice_init(struct td_list_head *list,
td_list_entry((pos)->member.prev, typeof(*(pos)), member)
+/*@
+ @ requires \valid(newe);
+ @ requires \valid(head);
+ @ requires \valid_function(compar);
+ @ requires separation: \separated(newe, head);
+ @*/
static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_head *head,
int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
{
@@ -387,6 +414,12 @@ static inline void td_list_add_sorted(struct td_list_head *newe, struct td_list_
td_list_add_tail(newe, head);
}
+/*@
+ @ requires \valid(newe);
+ @ requires \valid(head);
+ @ requires \valid_function(compar);
+ @ requires separation: \separated(newe, head);
+ @*/
static inline int td_list_add_sorted_uniq(struct td_list_head *newe, struct td_list_head *head,
int (*compar)(const struct td_list_head *a, const struct td_list_head *b))
{
diff --git a/src/memmem.h b/src/memmem.h
index d738dba..caa6873 100644
--- a/src/memmem.h
+++ b/src/memmem.h
@@ -22,6 +22,11 @@
*/
+/*@
+ @ requires \valid_read((const char *)haystack+(0..haystack_len-1));
+ @ requires \valid_read((const char *)needle+(0..needle_len-1));
+ @ assigns \nothing;
+ @*/
static inline const void *td_memmem(const void *haystack, const unsigned int haystack_len, const void *needle, const unsigned int needle_len)
{
const char *begin;
@@ -37,6 +42,9 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay
if (haystack_len < needle_len)
return NULL;
+ /*@
+ @ loop assigns begin;
+ @*/
for (begin = (const char *) haystack; begin <= last_possible; ++begin)
if (begin[0] == ((const char *) needle)[0] &&
!memcmp ((const void *) &begin[1],