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

src/file_ttf.c: Fix frama-c warnings

Browse source
This commit is contained in:
Christophe Grenier 2020-10-24 09:05:07 +02:00
parent 73ebc243b1
commit 9c3096c847
1 changed files with 30 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/file_ttf.c
View file

@ -64,9 +64,16 @@ struct ttf_table_directory
uint32_t length; /* Length of this table. */
};
/*@
@ assigns \nothing;
@*/
static unsigned int td_ilog2(unsigned int v)
{
unsigned int l = 0;
/*@
@ loop assigns v,l;
@ loop unroll 16;
@*/
while(v >>= 1)
l++;
return l;
@ -75,30 +82,45 @@ static unsigned int td_ilog2(unsigned int v)
static int header_check_ttf(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)
{
const struct ttf_offset_table *ttf=(const struct ttf_offset_table *)buffer;
unsigned int numTables;
numTables=be16(ttf->numTables);
const unsigned int numTables=be16(ttf->numTables);
const unsigned int entrySelector=be16(ttf->entrySelector);
const unsigned int searchRange=be16(ttf->searchRange);
const unsigned int rangeShift=be16(ttf->rangeShift);
if(numTables == 0)
return 0;
/* searchRange (Maximum power of 2 <= numTables) x 16.
* entrySelector Log2(maximum power of 2 <= numTables).
* rangeShift NumTables x 16-searchRange.
* */
if(td_ilog2(numTables) != (uint16_t)be16(ttf->entrySelector))
if(td_ilog2(numTables) != entrySelector)
return 0;
if((16<<be16(ttf->entrySelector)) != be16(ttf->searchRange))
if((16<<entrySelector) != searchRange)
return 0;
if(numTables * 16 != (unsigned int)be16(ttf->rangeShift)+be16(ttf->searchRange))
if(numTables * 16 != rangeShift+searchRange)
return 0;
reset_file_recovery(file_recovery_new);
file_recovery_new->extension=file_hint_ttf.extension;
if(sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory)
<= buffer_size)
{
const struct ttf_table_directory*ttf_dir=(const struct ttf_table_directory*)(ttf+1);
/*@ assert sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory) <= buffer_size; */
/*@ assert numTables * sizeof(struct ttf_table_directory) <= buffer_size - sizeof(struct ttf_offset_table); */
/*@ assert numTables <= (buffer_size - sizeof(struct ttf_offset_table)) / sizeof(struct ttf_table_directory); */
/*@ assert \valid_read(buffer + (0 .. buffer_size - 1)); */
/*@ assert \valid_read(buffer + (0 .. sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory) - 1)); */
uint64_t max_offset=0;
unsigned int i;
for(i=0; i<numTables; i++,ttf_dir++)
const struct ttf_table_directory*ttf_dir=(const struct ttf_table_directory*)&buffer[sizeof(struct ttf_offset_table)];
/*@ assert \valid_read(ttf_dir + (0 .. numTables -1)); */
/*@
@ loop assigns i, max_offset;
@*/
for(i=0; i<numTables; i++)
{
/*@ assert 0 <= i < numTables; */
/*@ assert \valid_read(&ttf_dir[i]); */
/* | 0x3: align the end of the table */
const uint64_t new_offset=(be32(ttf_dir->offset) + be32(ttf_dir->length))|0x3;
const uint64_t new_offset=((uint64_t)be32(ttf_dir[i].offset) + be32(ttf_dir[i].length))|0x3;
if(max_offset < new_offset)
max_offset=new_offset;
}