Split src/list.h in 3
This commit is contained in:
Christophe Grenier
parent
14210bd402
commit
0c9784cb76
7 changed files with 404 additions and 105 deletions
|
|
@ -39,7 +39,7 @@ EXTRA_PROGRAMS = photorecf fuzzerfidentify
|
|||
smallbase_C = common.c crc.c apfs_common.c ext2_common.c fat_common.c log.c misc.c setdate.c
|
||||
smallbase_H = common.h crc.h apfs_common.h ext2_common.h fat_common.h log.h misc.h setdate.h
|
||||
base_C = $(smallbase_C) autoset.c ewf.c fnctdsk.c hdaccess.c hdcache.c hdwin32.c hidden.c hpa_dco.c intrf.c iso.c list_sort.c log_part.c msdos.c parti386.c partgpt.c parthumax.c partmac.c partsun.c partnone.c partxbox.c io_redir.c ntfs_io.c ntfs_utl.c partauto.c sudo.c unicode.c win32.c
|
||||
base_H = $(smallbase_H) alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
|
||||
base_H = $(smallbase_H) apfs_common.h alignio.h autoset.h ewf.h fnctdsk.h hdaccess.h hdwin32.h hidden.h guid_cmp.h guid_cpy.h hdcache.h hpa_dco.h intrf.h iso.h iso9660.h lang.h list.h list_add_sorted.h list_add_sorted_uniq.h list_sort.h log_part.h types.h io_redir.h msdos.h ntfs_utl.h parti386.h partgpt.h parthumax.h partmac.h partsun.h partxbox.h partauto.h sudo.h unicode.h win32.h
|
||||
|
||||
fs_C = analyse.c apfs.c bfs.c bsd.c btrfs.c cramfs.c exfat.c ext2.c fat.c fatx.c f2fs.c jfs.c gfs2.c hfs.c hfsp.c hpfs.c luks.c lvm.c md.c netware.c ntfs.c refs.c rfs.c savehdr.c sun.c swap.c sysv.c ufs.c vmfs.c wbfs.c xfs.c zfs.c
|
||||
fs_H = analyse.h apfs.h bfs.h bsd.h btrfs.h cramfs.h exfat.h ext2.h fat.h fatx.h f2fs.h f2fs_fs.h jfs_superblock.h jfs.h gfs2.h hfs.h hfsp.h hpfs.h hfsp_struct.h luks.h luks_struct.h lvm.h md.h netware.h ntfs.h ntfs_struct.h refs.h rfs.h savehdr.h sun.h swap.h sysv.h ufs.h vmfs.h wbfs.h xfs.h xfs_struct.h zfs.h
|
||||
|
|
|
|||
|
|
@ -45,6 +45,72 @@
|
|||
#include "common.h"
|
||||
#include "log.h"
|
||||
|
||||
static int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
|
||||
|
||||
#ifndef __FRAMAC__
|
||||
#include "list_add_sorted.h"
|
||||
/*@ requires compar == signature_cmp; */
|
||||
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));
|
||||
#else
|
||||
/*@
|
||||
@ requires \valid(newe);
|
||||
@ requires \valid(head);
|
||||
@ requires separation: \separated(newe, head);
|
||||
@ requires list_separated(head->prev, newe);
|
||||
@ requires list_separated(head, newe);
|
||||
@ requires finite(head->prev);
|
||||
@ requires finite(head);
|
||||
@*/
|
||||
static inline void td_list_add_sorted_sig(struct td_list_head *newe, struct td_list_head *head)
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant \valid(pos);
|
||||
@ loop invariant \valid(pos->prev);
|
||||
@ loop invariant \valid(pos->next);
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
/*@ assert \valid_read(newe); */
|
||||
/*@ assert \valid_read(pos); */
|
||||
if(signature_cmp(newe,pos)<0)
|
||||
break;
|
||||
}
|
||||
if(pos != head)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
}
|
||||
else
|
||||
{
|
||||
/*@ assert finite(head->prev); */
|
||||
/*@ assert finite(head); */
|
||||
/*@ assert list_separated(head->prev, newe); */
|
||||
/*@ assert list_separated(head, newe); */
|
||||
td_list_add_tail(newe, head);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
/*@ requires valid_string_s: valid_read_string(s);
|
||||
@ ensures valid_string(\result);
|
||||
@*/
|
||||
static char *td_strdup(const char *s)
|
||||
{
|
||||
size_t l = strlen(s) + 1;
|
||||
char *p = (char *)MALLOC(l);
|
||||
/*@ assert valid_read_string(s); */
|
||||
memcpy(p, s, l);
|
||||
p[l-1]='\0';
|
||||
/*@ assert valid_read_string(p); */
|
||||
return p;
|
||||
}
|
||||
#endif
|
||||
|
||||
/*@ requires valid_register_header_check(file_stat); */
|
||||
static void register_header_check_sig(file_stat_t *file_stat);
|
||||
|
||||
const file_hint_t file_hint_sig= {
|
||||
|
|
@ -65,7 +131,7 @@ struct signature_s
|
|||
{
|
||||
struct td_list_head list;
|
||||
const char *extension;
|
||||
const unsigned char *sig;
|
||||
const char *sig;
|
||||
unsigned int sig_size;
|
||||
unsigned int offset;
|
||||
};
|
||||
|
|
@ -86,21 +152,25 @@ static signature_t signatures={
|
|||
.list = TD_LIST_HEAD_INIT(signatures.list)
|
||||
};
|
||||
|
||||
#ifndef __FRAMAC__
|
||||
static
|
||||
#endif
|
||||
int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
|
||||
/*@
|
||||
@ assigns \nothing;
|
||||
@*/
|
||||
static int signature_cmp(const struct td_list_head *a, const struct td_list_head *b)
|
||||
{
|
||||
const signature_t *sig_a=td_list_entry_const(a, const signature_t, list);
|
||||
const signature_t *sig_b=td_list_entry_const(b, const signature_t, list);
|
||||
int res;
|
||||
/*@ assert \valid_read(sig_a); */
|
||||
/*@ assert \valid_read(sig_b); */
|
||||
/*@ assert valid_signature(sig_a); */
|
||||
/*@ assert valid_signature(sig_b); */
|
||||
if(sig_a->sig_size==0 && sig_b->sig_size!=0)
|
||||
return -1;
|
||||
if(sig_a->sig_size!=0 && sig_b->sig_size==0)
|
||||
return 1;
|
||||
res=sig_a->offset-sig_b->offset;
|
||||
/*@ assert 0 <= sig_a->offset <= PHOTOREC_MAX_SIG_OFFSET; */
|
||||
/*@ assert 0 <= sig_b->offset <= PHOTOREC_MAX_SIG_OFFSET; */
|
||||
res=(int)sig_a->offset - (int)sig_b->offset;
|
||||
if(res!=0)
|
||||
return res;
|
||||
if(sig_a->sig_size<=sig_b->sig_size)
|
||||
|
|
@ -133,8 +203,9 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
|
|||
/*@ assert \valid_read((const char *)sig+(0..sig_size-1)); */
|
||||
/*@ assert valid_read_string(ext); */
|
||||
newsig=(signature_t*)MALLOC(sizeof(*newsig));
|
||||
/*@ assert \valid(newsig); */
|
||||
newsig->extension=ext;
|
||||
newsig->sig=(const unsigned char *)sig;
|
||||
newsig->sig=(const char *)sig;
|
||||
newsig->sig_size=sig_size;
|
||||
newsig->offset=offset;
|
||||
/*@ assert newsig->sig_size == sig_size; */
|
||||
|
|
@ -153,7 +224,11 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
|
|||
/*@ assert \valid_read((const char *)newsig->sig+(0..newsig->sig_size-1)); */
|
||||
|
||||
/*@ assert valid_signature(newsig); */
|
||||
#ifdef __FRAMAC__
|
||||
td_list_add_sorted_sig(&newsig->list, &signatures.list);
|
||||
#else
|
||||
td_list_add_sorted(&newsig->list, &signatures.list, signature_cmp);
|
||||
#endif
|
||||
}
|
||||
|
||||
/*@
|
||||
|
|
@ -165,10 +240,14 @@ static void signature_insert(const char *ext, unsigned int offset, const void*si
|
|||
static int header_check_sig(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@ loop assigns pos; */
|
||||
/*@
|
||||
@ loop invariant \valid(pos);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
td_list_for_each(pos, &signatures.list)
|
||||
{
|
||||
const signature_t *sig = td_list_entry(pos, signature_t, list);
|
||||
/*@ assert \valid_read(sig); */
|
||||
/*@ assert sig->offset + sig->sig_size <= buffer_size; */
|
||||
/*@ assert valid_read_string(sig->extension); */
|
||||
/*@ assert valid_signature(sig); */
|
||||
|
|
|
|||
114
src/filegen.c
114
src/filegen.c
|
|
@ -46,6 +46,57 @@
|
|||
#include "filegen.h"
|
||||
#include "log.h"
|
||||
|
||||
static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b);
|
||||
|
||||
#ifndef __FRAMAC__
|
||||
#include "list_add_sorted.h"
|
||||
/*@ requires compar == file_check_cmp; */
|
||||
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));
|
||||
#else
|
||||
|
||||
/*@
|
||||
@ requires \valid(newe);
|
||||
@ requires \valid(head);
|
||||
@ requires separation: \separated(newe, head);
|
||||
@ requires list_separated(head->prev, newe);
|
||||
@ requires list_separated(head, newe);
|
||||
@ requires finite(head->prev);
|
||||
@ requires finite(head);
|
||||
@*/
|
||||
static inline void td_list_add_sorted_fcc(struct td_list_head *newe, struct td_list_head *head)
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant \valid(pos);
|
||||
@ loop invariant \valid(pos->prev);
|
||||
@ loop invariant \valid(pos->next);
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
/*@ assert \valid_read(newe); */
|
||||
/*@ assert \valid_read(pos); */
|
||||
if(file_check_cmp(newe,pos)<0)
|
||||
break;
|
||||
}
|
||||
if(pos != head)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
}
|
||||
else
|
||||
{
|
||||
/*@ assert finite(head->prev); */
|
||||
/*@ assert finite(head); */
|
||||
/*@ assert list_separated(head->prev, newe); */
|
||||
/*@ assert list_separated(head, newe); */
|
||||
td_list_add_tail(newe, head);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
|
||||
uint64_t gpls_nbr=0;
|
||||
static uint64_t offset_skipped_header=0;
|
||||
|
||||
|
|
@ -57,16 +108,12 @@ file_check_list_t file_check_list={
|
|||
.list = TD_LIST_HEAD_INIT(file_check_list.list)
|
||||
};
|
||||
|
||||
// X requires \valid_read(b);
|
||||
/*@
|
||||
@ requires \valid_read(a);
|
||||
@ requires \valid_read(b);
|
||||
@ assigns \nothing;
|
||||
@*/
|
||||
#ifndef DISABLED_FOR_FRAMAC
|
||||
static
|
||||
#endif
|
||||
int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
|
||||
static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
|
||||
{
|
||||
#ifdef DISABLED_FOR_FRAMAC
|
||||
return 1;
|
||||
|
|
@ -149,6 +196,7 @@ void register_header_check(const unsigned int offset, const void *value, const u
|
|||
file_stat_t *file_stat)
|
||||
{
|
||||
file_check_t *file_check_new=(file_check_t *)MALLOC(sizeof(*file_check_new));
|
||||
/*@ assert \valid(file_check_new); */
|
||||
file_check_new->value=value;
|
||||
file_check_new->length=length;
|
||||
file_check_new->offset=offset;
|
||||
|
|
@ -166,7 +214,11 @@ void register_header_check(const unsigned int offset, const void *value, const u
|
|||
/*@ assert \valid(file_check_new->file_stat); */
|
||||
|
||||
/*@ assert valid_file_check_node(file_check_new); */
|
||||
#ifdef __FRAMAC__
|
||||
td_list_add_sorted_fcc(&file_check_new->list, &file_check_plist.list);
|
||||
#else
|
||||
td_list_add_sorted(&file_check_new->list, &file_check_plist.list, file_check_cmp);
|
||||
#endif
|
||||
}
|
||||
|
||||
/*@
|
||||
|
|
@ -187,9 +239,14 @@ static void index_header_check_aux(file_check_t *file_check_new)
|
|||
if(pos->offset >= file_check_new->offset &&
|
||||
pos->offset < file_check_new->offset+file_check_new->length)
|
||||
{
|
||||
#ifdef __FRAMAC__
|
||||
td_list_add_sorted_fcc(&file_check_new->list,
|
||||
&pos->file_checks[((const unsigned char *)file_check_new->value)[pos->offset-file_check_new->offset]].list);
|
||||
#else
|
||||
td_list_add_sorted(&file_check_new->list,
|
||||
&pos->file_checks[((const unsigned char *)file_check_new->value)[pos->offset-file_check_new->offset]].list,
|
||||
file_check_cmp);
|
||||
#endif
|
||||
return ;
|
||||
}
|
||||
if(pos->offset>file_check_new->offset)
|
||||
|
|
@ -319,6 +376,7 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
|
|||
memset(&buffer[4096],0,footer_length-1);
|
||||
/*@
|
||||
@ loop invariant 0 <= offset <= \at(offset, Pre);
|
||||
@ loop invariant offset <= PHOTOREC_MAX_FILE_SIZE;
|
||||
@ loop assigns errno, *handle, Frama_C_entropy_source;
|
||||
@ loop assigns offset, buffer[0 .. 8192-1];
|
||||
@ loop variant offset;
|
||||
|
|
@ -333,6 +391,7 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
|
|||
offset-=4096;
|
||||
else
|
||||
offset=offset-(offset%4096);
|
||||
/*@ assert offset + 4096 <= PHOTOREC_MAX_FILE_SIZE; */
|
||||
if(my_fseek(handle,offset,SEEK_SET)<0)
|
||||
return 0;
|
||||
taille=fread(&buffer, 1, 4096, handle);
|
||||
|
|
@ -342,9 +401,13 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
|
|||
#ifdef __FRAMAC__
|
||||
Frama_C_make_unknown(&buffer, 4096);
|
||||
#endif
|
||||
/*@ loop assigns i; */
|
||||
/*@
|
||||
@ loop invariant -1 <= i < taille;
|
||||
@ loop assigns i;
|
||||
@*/
|
||||
for(i=taille-1;i>=0;i--)
|
||||
{
|
||||
/*@ assert offset + i <= PHOTOREC_MAX_FILE_SIZE; */
|
||||
if(buffer[i]==*(const char *)footer && memcmp(&buffer[i],footer,footer_length)==0)
|
||||
{
|
||||
return offset + i;
|
||||
|
|
@ -357,17 +420,25 @@ 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)
|
||||
{
|
||||
/*@ assert \valid(file_recovery); */
|
||||
if(footer_length==0 || file_recovery->file_size <= extra_length)
|
||||
return ;
|
||||
file_recovery->file_size=file_rsearch(file_recovery->handle, file_recovery->file_size-extra_length, footer, footer_length);
|
||||
/*@ assert 0 < footer_length < 4096; */
|
||||
/*@ assert extra_length <= PHOTOREC_MAX_FILE_SIZE; */
|
||||
/*@ assert file_recovery->file_size < 0x8000000000000000; */
|
||||
if(file_recovery->file_size > 0)
|
||||
file_recovery->file_size+= footer_length + extra_length;
|
||||
file_recovery->file_size+= (uint64_t)footer_length + extra_length;
|
||||
/*@ assert \valid(file_recovery->handle); */
|
||||
/*@ assert valid_file_check_result(file_recovery); */
|
||||
}
|
||||
|
||||
data_check_t data_check_size(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
|
||||
{
|
||||
/*@ assert \valid_read(file_recovery); */
|
||||
/*@ assert valid_file_recovery(file_recovery); */
|
||||
/*@ assert file_recovery->file_size <= PHOTOREC_MAX_FILE_SIZE; */
|
||||
/*@ assert buffer_size <= 2 * PHOTOREC_MAX_BLOCKSIZE; */
|
||||
if(file_recovery->file_size + buffer_size/2 >= file_recovery->calculated_file_size)
|
||||
{
|
||||
/*@ assert valid_file_recovery(file_recovery); */
|
||||
|
|
@ -379,6 +450,7 @@ data_check_t data_check_size(const unsigned char *buffer, const unsigned int buf
|
|||
|
||||
void file_check_size(file_recovery_t *file_recovery)
|
||||
{
|
||||
/*@ assert \valid(file_recovery); */
|
||||
if(file_recovery->file_size<file_recovery->calculated_file_size)
|
||||
file_recovery->file_size=0;
|
||||
else
|
||||
|
|
@ -388,6 +460,7 @@ void file_check_size(file_recovery_t *file_recovery)
|
|||
|
||||
void file_check_size_min(file_recovery_t *file_recovery)
|
||||
{
|
||||
/*@ assert \valid(file_recovery); */
|
||||
if(file_recovery->file_size<file_recovery->calculated_file_size)
|
||||
file_recovery->file_size=0;
|
||||
/*@ assert valid_file_check_result(file_recovery); */
|
||||
|
|
@ -395,6 +468,7 @@ void file_check_size_min(file_recovery_t *file_recovery)
|
|||
|
||||
void file_check_size_max(file_recovery_t *file_recovery)
|
||||
{
|
||||
/*@ assert \valid(file_recovery); */
|
||||
if(file_recovery->file_size > file_recovery->calculated_file_size)
|
||||
file_recovery->file_size=file_recovery->calculated_file_size;
|
||||
/*@ assert valid_file_check_result(file_recovery); */
|
||||
|
|
@ -528,11 +602,14 @@ static int file_rename_aux(file_recovery_t *file_recovery, const char *new_ext)
|
|||
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires strlen((char*)&file_recovery->filename) < 1<<30;
|
||||
@ requires valid_file_recovery(file_recovery);
|
||||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires 0 <= offset < buffer_size;
|
||||
@ requires buffer_size < 1<<30;
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ ensures new_ext==\null || valid_read_string(new_ext);
|
||||
@ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
|
||||
@ ensures new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
|
||||
@ ensures valid_file_recovery(file_recovery);
|
||||
@*/
|
||||
static 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)
|
||||
|
|
@ -542,7 +619,7 @@ static int _file_rename(file_recovery_t *file_recovery, const void *buffer, cons
|
|||
const char *ext=NULL;
|
||||
char *dst;
|
||||
char *directory_sep;
|
||||
int len;
|
||||
size_t len;
|
||||
len=strlen(src)+1;
|
||||
/*@ assert offset < buffer_size; */
|
||||
len+=buffer_size-offset+1;
|
||||
|
|
@ -667,11 +744,14 @@ int file_rename(file_recovery_t *file_recovery, const void *buffer, const int bu
|
|||
/* The original filename begins at offset in buffer and is null terminated */
|
||||
/*@
|
||||
@ requires \valid(file_recovery);
|
||||
@ requires strlen((char*)&file_recovery->filename) < 1<<30;
|
||||
@ requires valid_file_recovery(file_recovery);
|
||||
@ requires valid_read_string((char*)&file_recovery->filename);
|
||||
@ requires 0 <= offset < buffer_size;
|
||||
@ requires buffer_size < 1<<30;
|
||||
@ requires \valid_read((char *)buffer+(0..buffer_size-1));
|
||||
@ requires new_ext==\null || valid_read_string(new_ext);
|
||||
@ requires new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
|
||||
@ ensures new_ext==\null || (valid_read_string(new_ext) && strlen(new_ext) < 1<<30);
|
||||
@ ensures valid_read_string((char*)&file_recovery->filename);
|
||||
@ ensures valid_file_recovery(file_recovery);
|
||||
@*/
|
||||
|
|
@ -682,7 +762,7 @@ static int _file_rename_unicode(file_recovery_t *file_recovery, const void *buff
|
|||
const char *src_ext=src;
|
||||
char *dst;
|
||||
char *dst_dir_sep;
|
||||
int len=strlen(src)+1;
|
||||
size_t len=strlen(src)+1;
|
||||
/*@ assert offset < buffer_size; */
|
||||
len+=buffer_size-offset;
|
||||
if(new_ext!=NULL)
|
||||
|
|
@ -855,6 +935,7 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
|
|||
}
|
||||
|
||||
/*@
|
||||
@ requires file_recovery_new == \null || \valid_read(file_recovery_new);
|
||||
@ requires \separated(file_recovery_new, &offset_skipped_header);
|
||||
@ assigns offset_skipped_header;
|
||||
@*/
|
||||
|
|
@ -865,6 +946,7 @@ void header_ignored(const file_recovery_t *file_recovery_new)
|
|||
offset_skipped_header=0;
|
||||
return ;
|
||||
}
|
||||
/*@ assert \valid_read(file_recovery_new); */
|
||||
if(file_recovery_new->location.start < offset_skipped_header || offset_skipped_header==0)
|
||||
offset_skipped_header=file_recovery_new->location.start;
|
||||
}
|
||||
|
|
@ -878,13 +960,18 @@ void get_prev_location_smart(const alloc_data_t *list_search_space, alloc_data_t
|
|||
alloc_data_t *file_space=*current_search_space;
|
||||
if(offset_skipped_header==0)
|
||||
return ;
|
||||
#ifndef __FRAMAC__
|
||||
gpls_nbr++;
|
||||
#endif
|
||||
/*@
|
||||
@ loop invariant \valid_read(file_space);
|
||||
@ loop invariant \separated(file_space, current_search_space, offset);
|
||||
@ loop assigns file_space, offset_skipped_header, *current_search_space, *offset;
|
||||
@*/
|
||||
while(1)
|
||||
{
|
||||
file_space=td_list_prev_entry(file_space, list);
|
||||
/*@ assert \valid_read(file_space); */
|
||||
if(file_space==list_search_space)
|
||||
break;
|
||||
if(file_space->start <= offset_skipped_header && offset_skipped_header < file_space->end)
|
||||
|
|
@ -903,11 +990,14 @@ void get_prev_location_smart(const alloc_data_t *list_search_space, alloc_data_t
|
|||
(long long unsigned)(*offset/512));
|
||||
#endif
|
||||
/*@
|
||||
@ loop invariant \valid_read(file_space);
|
||||
@ loop invariant \separated(file_space, current_search_space, offset);
|
||||
@ loop assigns file_space, offset_skipped_header, *current_search_space, *offset;
|
||||
@*/
|
||||
while(1)
|
||||
{
|
||||
file_space=td_list_prev_entry(file_space, list);
|
||||
/*@ assert \valid_read(file_space); */
|
||||
if(file_space==list_search_space)
|
||||
{
|
||||
offset_skipped_header=0;
|
||||
|
|
|
|||
143
src/list.h
143
src/list.h
|
|
@ -21,6 +21,7 @@
|
|||
*/
|
||||
#ifndef _LIST_H
|
||||
#define _LIST_H
|
||||
|
||||
/*
|
||||
* These are non-NULL pointers that will result in page faults
|
||||
* under normal circumstances, used to verify that nobody uses
|
||||
|
|
@ -44,37 +45,42 @@ struct td_list_head {
|
|||
struct td_list_head *next, *prev;
|
||||
};
|
||||
|
||||
#ifdef __FRAMAC__
|
||||
/*@
|
||||
@ requires \valid_read(a);
|
||||
@ requires \valid_read(b);
|
||||
@ assigns \nothing;
|
||||
@*/
|
||||
int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b);
|
||||
|
||||
/*@
|
||||
@ assigns \nothing;
|
||||
@*/
|
||||
int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
|
||||
#endif
|
||||
|
||||
/*@
|
||||
inductive reachable{L}(struct td_list_head *root, struct td_list_head *node) {
|
||||
case root_reachable{L}:
|
||||
\forall struct td_list_head *root; reachable(root,root) ;
|
||||
inductive reachable_forward{L}(struct td_list_head *root, struct td_list_head *node) {
|
||||
case root_reachable_forward{L}:
|
||||
\forall struct td_list_head *root; reachable_forward(root,root) ;
|
||||
case next_reachable{L}:
|
||||
\forall struct td_list_head *root,*node;
|
||||
\valid(root) && reachable(root->next,node) ==> reachable(root,node);
|
||||
\valid(root) && reachable_forward(root->next,node) ==> reachable_forward(root,node);
|
||||
}
|
||||
|
||||
inductive reachable_backward{L}(struct td_list_head *root, struct td_list_head *node) {
|
||||
case root_reachable_backward{L}:
|
||||
\forall struct td_list_head *root; reachable_backward(root,root) ;
|
||||
case prev_reachable{L}:
|
||||
\forall struct td_list_head *root,*node;
|
||||
\valid(root) && reachable_backward(root->prev,node) ==> reachable_backward(root,node);
|
||||
}
|
||||
@*/
|
||||
// root->next->prev == root
|
||||
|
||||
/*@ predicate finite{L}(struct td_list_head *root) = reachable(root->next,root); */
|
||||
/*@ predicate finite{L}(struct td_list_head *root) = reachable_forward(root->next,root) && reachable_backward(root->prev,root); */
|
||||
|
||||
|
||||
/*
|
||||
\forall struct td_list_head *l1;
|
||||
reachable(l, l1) && \valid(l1) ==> \valid(l1->next) && l1->next->prev == l1;
|
||||
*/
|
||||
/*@ inductive list_separated3{L}(struct td_list_head *root, struct td_list_head *node, struct td_list_head *elt) {
|
||||
case node_is_root{L}:
|
||||
\forall struct td_list_head *root, *elt; \separated(root, elt) ==> list_separated3(root, root, elt);
|
||||
case node_reachable{L}:
|
||||
\forall struct td_list_head *root, *node, *elt;
|
||||
\valid(node) && \separated(node, elt) && list_separated3(root, node->next, elt) ==> list_separated3(root, node, elt);
|
||||
}
|
||||
|
||||
*/
|
||||
/*@ predicate list_separated{L}(struct td_list_head *root, struct td_list_head *elt) = list_separated3(root, root->next, elt); */
|
||||
|
||||
#define TD_LIST_HEAD_INIT(name) { &(name), &(name) }
|
||||
|
||||
|
|
@ -97,10 +103,16 @@ int signature_cmp(const struct td_list_head *a, const struct td_list_head *b);
|
|||
@ requires \valid(next);
|
||||
@ requires separation: \separated(newe, \union(prev,next));
|
||||
@ requires prev == next || \separated(prev,next,newe);
|
||||
@ ensures next->prev == newe;
|
||||
@ ensures newe->next == next;
|
||||
@ ensures newe->prev == prev;
|
||||
@ requires finite(prev);
|
||||
@ requires finite(next);
|
||||
@ requires prev->next == next;
|
||||
@ requires next->prev == prev;
|
||||
@ requires list_separated(prev, newe);
|
||||
@ requires list_separated(next, newe);
|
||||
@ ensures prev->next == newe;
|
||||
@ ensures newe->prev == prev;
|
||||
@ ensures newe->next == next;
|
||||
@ ensures next->prev == newe;
|
||||
@ ensures newe->next->prev == newe;
|
||||
@ ensures newe->prev->next == newe;
|
||||
@ assigns next->prev,newe->next,newe->prev,prev->next;
|
||||
|
|
@ -109,14 +121,24 @@ static inline void __td_list_add(struct td_list_head *newe,
|
|||
struct td_list_head *prev,
|
||||
struct td_list_head *next)
|
||||
{
|
||||
/*@ assert finite(prev); */
|
||||
/*@ assert finite(next); */
|
||||
/*@ assert reachable_forward(prev->next,prev); */
|
||||
/*@ assert reachable_forward(next->next,next); */
|
||||
/*@ assert reachable_backward(prev->prev,prev); */
|
||||
/*@ assert reachable_backward(next->prev,next); */
|
||||
|
||||
/*@ assert reachable_forward(next,prev); */
|
||||
newe->next = next;
|
||||
newe->prev = prev;
|
||||
next->prev = newe;
|
||||
prev->next = newe;
|
||||
next->prev = newe;
|
||||
/*@ assert next->prev == newe; */
|
||||
/*@ assert newe->next == next; */
|
||||
/*@ assert newe->prev == prev; */
|
||||
/*@ assert prev->next == newe; */
|
||||
/*@ assert reachable_forward(prev,newe); */
|
||||
/*@ assert reachable_backward(next,newe); */
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -132,6 +154,9 @@ static inline void __td_list_add(struct td_list_head *newe,
|
|||
@ requires \valid(head);
|
||||
@ requires \valid(head->next);
|
||||
@ requires separation: \separated(newe, \union(head,head->next));
|
||||
@ requires finite(head);
|
||||
@ requires finite(head->next);
|
||||
@ requires list_separated(head, newe);
|
||||
@ ensures head->next == newe;
|
||||
@ ensures newe->prev == head;
|
||||
@ ensures newe->next == \old(head->next);
|
||||
|
|
@ -155,8 +180,13 @@ 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);
|
||||
@ requires \separated(newe, \union(head->prev, head));
|
||||
@ requires head->prev == head || \separated(head->prev, head, newe);
|
||||
@ requires finite(head->prev);
|
||||
@ requires list_separated(head->prev, newe);
|
||||
@ requires list_separated(head, newe);
|
||||
@ requires finite(head);
|
||||
@ ensures head->prev == newe;
|
||||
@ ensures newe->next == head;
|
||||
@ ensures newe->prev == \old(head->prev);
|
||||
|
|
@ -218,6 +248,7 @@ static inline void td_list_del(struct td_list_head *entry)
|
|||
/*@ assert \at(entry->next,Pre)->prev == \at(entry->prev,Pre); */
|
||||
}
|
||||
|
||||
#if 0
|
||||
/**
|
||||
* td_list_del_init - deletes entry from list and reinitialize it.
|
||||
* @entry: the element to delete from the list.
|
||||
|
|
@ -227,7 +258,9 @@ static inline void td_list_del_init(struct td_list_head *entry)
|
|||
__td_list_del(entry->prev, entry->next);
|
||||
TD_INIT_LIST_HEAD(entry);
|
||||
}
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
/**
|
||||
* td_list_move - delete from one list and add as another's head
|
||||
* @list: the entry to move
|
||||
|
|
@ -250,6 +283,7 @@ static inline void td_list_move_tail(struct td_list_head *list,
|
|||
__td_list_del(list->prev, list->next);
|
||||
td_list_add_tail(list, head);
|
||||
}
|
||||
#endif
|
||||
|
||||
/**
|
||||
* td_list_empty - tests whether a list is empty
|
||||
|
|
@ -264,6 +298,7 @@ static inline int td_list_empty(const struct td_list_head *head)
|
|||
return head->next == head;
|
||||
}
|
||||
|
||||
#if 0
|
||||
/**
|
||||
* td_list_empty_careful - tests whether a list is
|
||||
* empty _and_ checks that no other CPU might be
|
||||
|
|
@ -322,6 +357,7 @@ static inline void td_list_splice_init(struct td_list_head *list,
|
|||
TD_INIT_LIST_HEAD(list);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
/**
|
||||
* td_list_entry - get the struct for this entry
|
||||
|
|
@ -473,67 +509,6 @@ 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 compar == signature_cmp || compar == file_check_cmp;
|
||||
@ 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))
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop invariant compar == signature_cmp || compar == file_check_cmp;
|
||||
@*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
/*@ assert compar == signature_cmp || compar == file_check_cmp; */
|
||||
/*@ assert \valid_read(newe); */
|
||||
/*@ assert \valid_read(pos); */
|
||||
if(compar(newe,pos)<0)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
return ;
|
||||
}
|
||||
}
|
||||
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))
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop invariant \valid_function(compar);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
// TODO const
|
||||
/* calls spacerange_cmp; */
|
||||
int res=compar(newe,pos);
|
||||
if(res<0)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
return 0;
|
||||
}
|
||||
else if(res==0)
|
||||
return 1;
|
||||
}
|
||||
td_list_add_tail(newe, head);
|
||||
return 0;
|
||||
}
|
||||
|
||||
typedef struct alloc_list_s alloc_list_t;
|
||||
struct alloc_list_s
|
||||
{
|
||||
|
|
|
|||
80
src/list_add_sorted.h
Normal file
80
src/list_add_sorted.h
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
/*
|
||||
|
||||
File: list_add_sorted.h
|
||||
|
||||
Copyright (C) 2006-2008 Christophe GRENIER <grenier@cgsecurity.org>
|
||||
|
||||
This software is free software; you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation; either version 2 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License along
|
||||
with this program; if not, write the Free Software Foundation, Inc., 51
|
||||
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
|
||||
|
||||
*/
|
||||
#ifndef _LIST_ADD_SORTED_UNIQ_H
|
||||
#define _LIST_ADD_SORTED_UNIQ_H
|
||||
|
||||
/*
|
||||
X requires finite(head);
|
||||
X ensures finite(head);
|
||||
X ensures finite(newe);
|
||||
X ensures reachable(head,newe);
|
||||
*/
|
||||
/*@
|
||||
@ requires \valid(newe);
|
||||
@ requires \valid(head);
|
||||
@ requires \valid_function(compar);
|
||||
@ requires separation: \separated(newe, head);
|
||||
@ requires list_separated(head->prev, newe);
|
||||
@ requires list_separated(head, newe);
|
||||
@ requires finite(head->prev);
|
||||
@ requires finite(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))
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant \valid(pos);
|
||||
@ loop invariant \valid(pos->prev);
|
||||
@ loop invariant \valid(pos->next);
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop invariant \valid_function(compar);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
/*
|
||||
X loop invariant finite(head->prev);
|
||||
X loop invariant finite(head);
|
||||
*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
/*@ assert \valid_function(compar); */
|
||||
/*@ assert \valid_read(newe); */
|
||||
/*@ assert \valid_read(pos); */
|
||||
if(compar(newe,pos)<0)
|
||||
break;
|
||||
}
|
||||
if(pos != head)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
}
|
||||
else
|
||||
{
|
||||
/*@ assert finite(head->prev); */
|
||||
/*@ assert finite(head); */
|
||||
/*@ assert list_separated(head->prev, newe); */
|
||||
/*@ assert list_separated(head, newe); */
|
||||
td_list_add_tail(newe, head);
|
||||
}
|
||||
/*X assert finite(head); */
|
||||
/*X assert finite(newe); */
|
||||
}
|
||||
#endif
|
||||
74
src/list_add_sorted_uniq.h
Normal file
74
src/list_add_sorted_uniq.h
Normal file
|
|
@ -0,0 +1,74 @@
|
|||
/*
|
||||
|
||||
File: list_add_sorted_uniq.h
|
||||
|
||||
Copyright (C) 2006-2008 Christophe GRENIER <grenier@cgsecurity.org>
|
||||
|
||||
This software is free software; you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation; either version 2 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License along
|
||||
with this program; if not, write the Free Software Foundation, Inc., 51
|
||||
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
|
||||
|
||||
*/
|
||||
#ifndef _LIST_ADD_SORTED_UNIQ_H
|
||||
#define _LIST_ADD_SORTED_UNIQ_H
|
||||
|
||||
/*@
|
||||
@ requires \valid(newe);
|
||||
@ requires \valid(head);
|
||||
@ requires \valid_function(compar);
|
||||
@ requires finite(head->prev);
|
||||
@ requires finite(head);
|
||||
@ requires separation: \separated(newe, head);
|
||||
@ requires list_separated(head, newe);
|
||||
@*/
|
||||
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))
|
||||
{
|
||||
struct td_list_head *pos;
|
||||
/*@
|
||||
@ loop invariant \valid(pos);
|
||||
@ loop invariant \valid(pos->prev);
|
||||
@ loop invariant \valid(pos->next);
|
||||
@ loop invariant pos == head || \separated(pos, head);
|
||||
@ loop invariant \valid_function(compar);
|
||||
@ loop invariant finite(head->prev);
|
||||
@ loop invariant finite(head);
|
||||
@ loop invariant finite(pos->prev);
|
||||
@ loop invariant finite(pos);
|
||||
@ loop assigns pos;
|
||||
@*/
|
||||
td_list_for_each(pos, head)
|
||||
{
|
||||
/*@ assert \valid_function(compar); */
|
||||
// TODO const
|
||||
/* calls spacerange_cmp; */
|
||||
int res=compar(newe,pos);
|
||||
/*@ assert \valid(pos); */
|
||||
/*@ assert \valid(pos->prev); */
|
||||
/*@ assert \valid(pos->next); */
|
||||
if(res<0)
|
||||
{
|
||||
__td_list_add(newe, pos->prev, pos);
|
||||
return 0;
|
||||
}
|
||||
else if(res==0)
|
||||
return 1;
|
||||
}
|
||||
/*@ assert finite(head->prev); */
|
||||
/*@ assert finite(head); */
|
||||
/*@ assert list_separated(head->prev, newe); */
|
||||
/*@ assert list_separated(head, newe); */
|
||||
td_list_add_tail(newe, head);
|
||||
return 0;
|
||||
}
|
||||
#endif
|
||||
|
|
@ -42,6 +42,7 @@ extern int need_to_stop;
|
|||
#include "geometry.h"
|
||||
#include "poptions.h"
|
||||
#include "phcli.h"
|
||||
#include "list_add_sorted_uniq.h"
|
||||
|
||||
typedef enum { INIT_SPACE_WHOLE, INIT_SPACE_PREINIT, INIT_SPACE_EXT2_GROUP, INIT_SPACE_EXT2_INODE } init_mode_t;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue