summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-01-26 16:36:08 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2020-01-26 16:36:08 +0100
commit351babdc434fe211360257bba50550ac35657ab0 (patch)
treece5a78171e0fcb36b508384feff957a2eba89fdd
parent4df871bf15bd29319eeb127af798ebe13c0ffc5a (diff)
frama-c: annotate file_check_add_tail() and td_list_add()
-rw-r--r--src/filegen.c16
-rw-r--r--src/list.h1
2 files changed, 16 insertions, 1 deletions
diff --git a/src/filegen.c b/src/filegen.c
index db9fca9..26ef872 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -85,17 +85,31 @@ static int file_check_cmp(const struct td_list_head *a, const struct td_list_hea
return (int)fc_b->length-(int)fc_a->length;
}
+/*@
+ @ requires \valid(file_check_new);
+ @ requires \valid(pos);
+ @*/
static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t *pos)
{
unsigned int i;
+ const unsigned int tmp=(file_check_new->length==0?0:((const unsigned char *)file_check_new->value)[0]);
file_check_list_t *newe=(file_check_list_t *)MALLOC(sizeof(*newe));
newe->offset=file_check_new->offset;
+ /*@
+ @ loop unroll 256;
+ @ loop invariant 0 <= i <= 256;
+ @ loop assigns i, newe->file_checks[0 .. 255].list.prev, newe->file_checks[0 .. 255].list.next;
+ @ loop variant 255-i;
+ @*/
for(i=0;i<256;i++)
{
newe->file_checks[i].list.prev=&newe->file_checks[i].list;
newe->file_checks[i].list.next=&newe->file_checks[i].list;
+ /*@ assert newe->file_checks[i].list.prev == &newe->file_checks[i].list; */
+ /*@ assert newe->file_checks[i].list.next == &newe->file_checks[i].list; */
}
- td_list_add_tail(&file_check_new->list, &newe->file_checks[file_check_new->length==0?0:((const unsigned char *)file_check_new->value)[0]].list);
+ /*@ assert newe->file_checks[tmp].list.prev == &newe->file_checks[tmp].list; */
+ td_list_add_tail(&file_check_new->list, &newe->file_checks[tmp].list);
td_list_add_tail(&newe->list, &pos->list);
}
diff --git a/src/list.h b/src/list.h
index 2cd2995..265e7fe 100644
--- a/src/list.h
+++ b/src/list.h
@@ -104,6 +104,7 @@ static inline void td_list_add(struct td_list_head *newe, struct td_list_head *h
/*@
@ requires \valid(newe);
@ requires \valid(head);
+ @ requires \valid(head->prev);
@ requires separation: \separated(newe, head);
@ ensures head->prev == newe;
@ ensures newe->next == head;