luisgulo/testdisk
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

frama-c: annotate file_check_add_tail() and td_list_add()

Browse source
This commit is contained in:
Christophe Grenier 2020-01-26 16:36:08 +01:00
parent 4df871bf15
commit 351babdc43
2 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/filegen.c
View file

@ -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);
}

1
src/list.h
View file

@ -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;