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

Commit various Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2023-02-19 09:15:52 +01:00
parent 97f7083ba8
commit 5ddaee9a47
9 changed files with 103 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/common.c
View file

@ -212,6 +212,7 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
unsigned int i;
/*@
@ loop assigns i, partition->fsname[i];
@ loop invariant 0 <= i < sizeof(partition->fsname);
@*/
for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
partition->fsname[i]=src[i];
@ -223,6 +224,7 @@ void set_part_name_chomp(partition_t *partition, const unsigned char *src, const
unsigned int i;
/*@
@ loop assigns i, partition->fsname[i];
@ loop invariant 0 <= i < sizeof(partition->fsname);
@*/
for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
partition->fsname[i]=src[i];
@ -375,6 +377,7 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
unsigned int i;
/*@
@ loop invariant valid_read_string(src);
@ loop invariant 0 <= i <= n;
@ loop assigns i, src;
@*/
for(i=0; i<n && src[0]!='\0'; i++)

2
src/common.h
View file

@ -31,7 +31,6 @@ extern "C" {
#include <string.h>
#endif
typedef struct efi_guid_s efi_guid_t;
struct efi_guid_s
{
uint32_t time_low;
@ -41,6 +40,7 @@ struct efi_guid_s
uint8_t clock_seq_low;
uint8_t node[6];
} __attribute__ ((gcc_struct, __packed__));
typedef struct efi_guid_s efi_guid_t;
#define DEFAULT_SECTOR_SIZE 0x200u

4
src/crc.c
View file

@ -91,9 +91,11 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
register uint32_t crc32val;
const unsigned char *s=(const unsigned char *)buf;
crc32val = seed;
/*@ loop assigns i, crc32val; */
/*@ loop invariant 0 <= i <= len;
@ loop assigns i, crc32val; */
for (i = 0; i < len; i ++)
{
/*@ assert i < len; */
crc32val = crc32_tab[(crc32val ^ s[i]) & 0xff] ^ (crc32val >> 8);
}
return (unsigned int)crc32val;

2
src/file_dst.c
View file

@ -58,7 +58,7 @@ static int header_check_dst(const unsigned char *buffer, const unsigned int buff
buf[7]='\0';
if(memcmp(buffer, "LA:",3)!=0 || memcmp(&buffer[30], "\rCO:", 4)!=0)
return 0;
if(sscanf(&buf, "%u", &stitch_count) < 0)
if(sscanf(&buf[0], "%u", &stitch_count) < 0)
return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_dst.extension;

1
src/file_flv.c
View file

@ -66,6 +66,7 @@ struct flv_tag
/*@
@ requires file_recovery->data_check==&data_check_flv;
@ requires valid_data_check_param(buffer, buffer_size, file_recovery);
@ ensures valid_data_check_param(buffer, buffer_size, file_recovery);
@ ensures valid_data_check_result(\result, file_recovery);
@ assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
@*/

11
src/file_template.c
View file

@ -31,7 +31,7 @@
#include "types.h"
#include "filegen.h"
/*@ requires \valid(file_stat); */
/*@ requires valid_register_header_check(file_stat); */
static void register_header_check_EXTENSION(file_stat_t *file_stat);
const file_hint_t file_hint_EXTENSION= {
@ -43,6 +43,11 @@ const file_hint_t file_hint_EXTENSION= {
.register_header_check=&register_header_check_EXTENSION
};
/*@
@ requires valid_file_check_param(file_recovery);
@ ensures valid_file_check_result(file_recovery);
@ assigns *file_recovery_new;
@*/
static void file_check_EXTENSION(file_recovery_t *file_recovery)
{
const unsigned char EXTENSION_footer[FOOTER_SIZE]= {
@ -51,6 +56,10 @@ static void file_check_EXTENSION(file_recovery_t *file_recovery)
file_search_footer(file_recovery, EXTENSION_footer, sizeof(EXTENSION_footer), FOOTER_EXTRA);
}
/*@
@ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
@ ensures valid_header_check_result(\result, file_recovery_new);
@*/
static int header_check_EXTENSION(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)
{
reset_file_recovery(file_recovery_new);

105
src/fnctdsk.h
View file

@ -27,18 +27,22 @@ extern "C" {
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ assigns \nothing;
@*/
unsigned long int C_H_S2LBA(const disk_t *disk_car,const unsigned int C, const unsigned int H, const unsigned int S);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid_read(CHS);
@ assigns \nothing;
@*/
uint64_t CHS2offset(const disk_t *disk_car,const CHS_t*CHS);
uint64_t CHS2offset(const disk_t *disk_car, const CHS_t*CHS);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->geom.sectors_per_head > 0;
@ assigns \nothing;
@ -48,6 +52,7 @@ unsigned int offset2sector(const disk_t *disk_car, const uint64_t offset);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->geom.sectors_per_head > 0;
@ requires disk_car->geom.heads_per_cylinder > 0;
@ -58,6 +63,7 @@ unsigned int offset2head(const disk_t *disk_car, const uint64_t offset);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires disk_car->sector_size > 0;
@ requires disk_car->geom.sectors_per_head > 0;
@ requires disk_car->geom.heads_per_cylinder > 0;
@ -67,78 +73,84 @@ unsigned int offset2cylinder(const disk_t *disk_car, const uint64_t offset);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid(CHS);
@ requires disk_car->sector_size > 0;
@ requires disk_car->geom.sectors_per_head > 0;
@ requires disk_car->geom.heads_per_cylinder > 0;
@ requires \separated(disk_car, CHS);
@ assigns CHS->cylinder,CHS->head,CHS->sector;
@*/
void offset2CHS(const disk_t *disk_car,const uint64_t offset, CHS_t*CHS);
/*@
@ requires list_disk==\null || \valid(list_disk);
@ requires disk==\null || (\valid(disk) && valid_read_string(disk->device));
@ requires the_disk==\null || \valid(the_disk);
@ ensures \result==\null || \valid(\result);
@ ensures disk==\null ==> \result == list_disk;
@ requires valid_list_disk(list_disk);
@ requires \valid(disk);
@ requires valid_disk(disk);
@ requires disk==\null || \separated(disk, \union(list_disk, the_disk));
@ requires the_disk==\null || (\valid_read(the_disk) && valid_disk(*the_disk) && \separated(the_disk, \union(list_disk, disk)));
@ decreases 0;
@*/
// ensures \result==\null || (\valid(\result) && valid_disk(\result->disk));
// ensures valid_list_disk(\result);
// ensures disk==\null ==> \result == list_disk;
// ensures the_disk==\null || (\valid_read(the_disk) && valid_disk(*the_disk));
list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk);
/*@
@ requires list_disk==\null || \valid(list_disk);
@ requires disk_car==\null || (\valid(disk_car) && valid_read_string(disk_car->device));
@ ensures \result==\null || \valid(\result);
@ requires list_disk==\null || valid_disk(list_disk->disk);
@ requires \valid(disk_car);
@ requires valid_disk(disk_car);
@ requires valid_list_disk(list_disk);
@ requires (list_disk==\null && disk_car==\null) || \separated(list_disk, disk_car);
@*/
// ensures \result==\null || (\valid(\result) && valid_disk(\result->disk));
// ensures disk_car==\null ==> \result == list_disk;
// ensures valid_list_disk(\result);
list_disk_t *insert_new_disk(list_disk_t *list_disk, disk_t *disk_car);
/*@
@ requires list_part == \null || \valid(list_part);
@ requires \valid(part);
@ requires valid_list_part(list_part);
@ requires valid_partition(part);
@ requires \valid(insert_error);
@ requires (list_part==\null && part==\null) || \separated(list_part, part);
@ requires insert_error==\null || \valid(insert_error);
@*/
// ensures valid_list_part(\result);
list_part_t *insert_new_partition(list_part_t *list_part, partition_t *part, const int force_insert, int *insert_error);
/*@
@ requires \valid(list_part);
@ requires valid_list_part(list_part);
@ ensures valid_list_part(\result);
@*/
list_part_t *sort_partition_list(list_part_t *list_part);
/*@
@ requires \valid_read(list_part);
@ requires valid_list_part(list_part);
@ ensures valid_list_part(\result);
@*/
list_part_t *gen_sorted_partition_list(const list_part_t *list_part);
/*@
@ requires \valid(list_part);
@ requires valid_list_part(list_part);
@*/
void part_free_list(list_part_t *list_part);
/*@
@ requires \valid(list_part);
@ requires valid_list_part(list_part);
@*/
void part_free_list_only(list_part_t *list_part);
/*@
@ requires \valid(partition);
@ requires valid_partition(partition);
@ requires \valid_read(arch);
@ assigns partition->part_size;
@ assigns partition->sborg_offset;
@ assigns partition->sb_offset;
@ assigns partition->sb_size;
@ assigns partition->blocksize;
@ assigns partition->part_type_i386;
@ assigns partition->part_type_sun;
@ assigns partition->part_type_mac;
@ assigns partition->part_type_xbox;
@ assigns partition->part_type_gpt;
@ assigns partition->part_uuid;
@ assigns partition->upart_type;
@ assigns partition->status;
@ assigns partition->order;
@ assigns partition->errcode;
@ assigns partition->fsname[0];
@ assigns partition->partname[0];
@ assigns partition->info[0];
@ requires \separated(partition, arch);
@ ensures partition->part_size == 0;
@ ensures partition->sborg_offset == 0;
@ ensures partition->sb_offset == 0;
@ -157,23 +169,44 @@ void part_free_list_only(list_part_t *list_part);
@ ensures partition->info[0] == '\0';
@ ensures partition->arch == arch;
@*/
// assigns partition->part_size;
// assigns partition->sborg_offset;
// assigns partition->sb_offset;
// assigns partition->sb_size;
// assigns partition->blocksize;
// assigns partition->part_type_i386;
// assigns partition->part_type_sun;
// assigns partition->part_type_mac;
// assigns partition->part_type_xbox;
// assigns partition->part_type_gpt;
// assigns partition->part_uuid;
// assigns partition->upart_type;
// assigns partition->status;
// assigns partition->order;
// assigns partition->errcode;
// assigns partition->fsname[0];
// assigns partition->partname[0];
// assigns partition->info[0];
void partition_reset(partition_t *partition, const arch_fnct_t *arch);
/*@
@ requires \valid_read(arch);
@ ensures \result->arch == arch;
@*/
// ensures valid_partition(\result);
// ensures \result->arch == arch;
partition_t *partition_new(const arch_fnct_t *arch);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid_read(list_part);
@ assigns \nothing;
@ requires valid_list_part(list_part);
@*/
// assigns \nothing;
unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part_t *list_part, const int verbose);
/*@
@ requires list_disk==\null || \valid(list_disk);
@ requires valid_list_disk(list_disk);
@ requires list_disk==\null || \freeable(list_disk);
@ requires list_disk==\null || \freeable(list_disk->disk);
@ requires list_disk==\null || (list_disk->disk->device == \null || \freeable(list_disk->disk->device));
@ -183,18 +216,20 @@ unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part
@ requires list_disk==\null || (list_disk->disk->data == \null || \freeable(list_disk->disk->data));
@ requires list_disk==\null || (list_disk->disk->rbuffer == \null || \freeable(list_disk->disk->rbuffer));
@ requires list_disk==\null || (list_disk->disk->wbuffer == \null || \freeable(list_disk->disk->wbuffer));
@ decreases 0;
@*/
int delete_list_disk(list_disk_t *list_disk);
/*@
@ requires \valid(buffer + (0..99));
@ ensures valid_string(buffer);
@ assigns buffer[0 .. 99];
@*/
/* TODO assigns */
void size_to_unit(const uint64_t disk_size, char *buffer);
/*@
@ requires \valid_read(list_part);
@ requires valid_list_part(list_part);
@ assigns \nothing;
@*/
int is_part_overlapping(const list_part_t *list_part);
@ -202,11 +237,15 @@ int is_part_overlapping(const list_part_t *list_part);
/*@
@ requires \valid(dest);
@ requires \valid_read(src);
@ requires \separated(src, dest);
@ requires valid_partition(src);
@ ensures valid_partition(dest);
@*/
void dup_partition_t(partition_t *dest, const partition_t *src);
/*@
@ requires list_disk==\null || \valid(list_disk);
@ requires valid_list_disk(list_disk);
@ assigns \nothing;
@*/
void log_disk_list(list_disk_t *list_disk);
#ifdef __cplusplus

2
src/log.c
View file

@ -227,6 +227,7 @@ void dump_log(const void *nom_dump, const unsigned int lng)
unsigned int i,j;
unsigned int nbr_line;
unsigned char car;
/*@ assert lng < UINT_MAX - 0x10; */
nbr_line=(lng+0x10-1)/0x10;
/* write dump to log file*/
for (i=0; (i<nbr_line); i++)
@ -266,6 +267,7 @@ void dump2_log(const void *dump_1, const void *dump_2, const unsigned int lng)
{
unsigned int i,j;
unsigned int nbr_line;
/*@ requires lng < UINT_MAX - 0x08; */
nbr_line=(lng+0x08-1)/0x08;
/* write dump to log file*/
for (i=0; (i<nbr_line); i++)

13
src/partgpt.h
View file

@ -24,6 +24,7 @@
#ifdef __cplusplus
extern "C" {
#endif
#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
struct gpt_hdr
{
@ -63,21 +64,27 @@ struct systypes_gtp {
};
/*@
@ requires valid_disk(disk_car);
@ requires \valid_read(disk_car);
@ requires \valid(list_part);
@ requires separation: \separated(disk_car, list_part, current_cmd);
@ requires valid_list_part(list_part);
@ requires \valid(current_cmd);
@ requires valid_string(*current_cmd);
@ requires separation: \separated(disk_car, list_part, current_cmd, *current_cmd);
@ requires valid_read_string(*current_cmd);
@*/
// ensures valid_list_part(\result);
// ensures valid_read_string(*current_cmd);
list_part_t *add_partition_gpt_cli(const disk_t *disk_car, list_part_t *list_part, char **current_cmd);
/*@
@ requires \valid_read(disk_car);
@ requires valid_disk(disk_car);
@ requires \valid(list_part);
@ requires valid_list_part(list_part);
@ requires separation: \separated(disk_car, list_part);
@*/
int write_part_gpt(disk_t *disk_car, const list_part_t *list_part, const int ro, const int verbose);
#endif
#ifdef __cplusplus
} /* closing brace for extern "C" */
#endif