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

src/fat_common.[ch]: update Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-06-12 13:22:19 +02:00
parent 261c73bb72
commit 12c2aabaa3
2 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/fat_common.c
View file

@ -31,13 +31,25 @@
#include "fat_common.h"
unsigned int fat_sector_size(const struct fat_boot_sector *fat_header)
{ return (fat_header->sector_size[1]<<8)+fat_header->sector_size[0]; }
{
const unsigned int res=(fat_header->sector_size[1]<<8)+fat_header->sector_size[0];
/*@ assert res <= 65535; */
return res;
}
unsigned int get_dir_entries(const struct fat_boot_sector *fat_header)
{ return (fat_header->dir_entries[1]<<8)+fat_header->dir_entries[0]; }
{
const unsigned int res=(fat_header->dir_entries[1]<<8)+fat_header->dir_entries[0];
/*@ assert res <= 65535; */
return res;
}
unsigned int fat_sectors(const struct fat_boot_sector *fat_header)
{ return (fat_header->sectors[1]<<8)+fat_header->sectors[0]; }
{
const unsigned int res=(fat_header->sectors[1]<<8)+fat_header->sectors[0];
/*@ assert res <= 65535; */
return res;
}
unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry)
{

7
src/fat_common.h
View file

@ -136,6 +136,7 @@ struct msdos_dir_slot {
/*@
@ requires \valid_read(entry);
@ requires \initialized(entry);
@ assigns \nothing;
@ */
unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry);
@ -148,18 +149,24 @@ int is_fat_directory(const unsigned char *buffer);
/*@
@ requires \valid_read(fat_header);
@ requires \initialized(fat_header);
@ ensures \result <= 65535;
@ assigns \nothing;
@ */
unsigned int get_dir_entries(const struct fat_boot_sector *fat_header);
/*@
@ requires \valid_read(fat_header);
@ requires \initialized(fat_header);
@ ensures \result <= 65535;
@ assigns \nothing;
@ */
unsigned int fat_sector_size(const struct fat_boot_sector *fat_header);
/*@
@ requires \valid_read(fat_header);
@ requires \initialized(fat_header);
@ ensures \result <= 65535;
@ assigns \nothing;
@ */
unsigned int fat_sectors(const struct fat_boot_sector *fat_header);