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

src/file_nk2.c: fix Frama-C annotations for file_check_nk2()

Browse source
This commit is contained in:
Christophe Grenier 2023-10-08 14:34:41 +02:00
parent 2ddc089e4d
commit 2dfa134455
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/file_nk2.c
View file

@ -100,6 +100,8 @@ static void file_check_nk2(file_recovery_t *fr)
char buf_nk2h[sizeof(nk2Header)]; char buf_nk2h[sizeof(nk2Header)];
const nk2Header *nk2h=(const nk2Header *)&buf_nk2h; const nk2Header *nk2h=(const nk2Header *)&buf_nk2h;
unsigned int i; unsigned int i;
/*@ assert \valid(fr); */
/*@ assert \valid_read(nk2h); */
fr->file_size = 0; fr->file_size = 0;
fr->offset_error=0; fr->offset_error=0;
fr->offset_ok=0; fr->offset_ok=0;
@ -123,6 +125,7 @@ static void file_check_nk2(file_recovery_t *fr)
unsigned int j; unsigned int j;
char buf_itemh[sizeof(itemHeader)]; char buf_itemh[sizeof(itemHeader)];
const itemHeader *itemh=(const itemHeader *)&buf_itemh; const itemHeader *itemh=(const itemHeader *)&buf_itemh;
/*@ assert \valid_read(itemh); */
if(fr->file_size >= NK2_MAX_FILESIZE) if(fr->file_size >= NK2_MAX_FILESIZE)
{ {
fr->file_size=0; fr->file_size=0;
@ -152,6 +155,7 @@ static void file_check_nk2(file_recovery_t *fr)
uint64_t size; uint64_t size;
char buf_entryh[sizeof(entryHeader)]; char buf_entryh[sizeof(entryHeader)];
const entryHeader *entryh=(const entryHeader *)&buf_entryh; const entryHeader *entryh=(const entryHeader *)&buf_entryh;
/*@ assert \valid_read(entryh); */
if (fread(&buf_entryh, sizeof(entryHeader), 1, fr->handle)!=1) if (fread(&buf_entryh, sizeof(entryHeader), 1, fr->handle)!=1)
{ {
fr->offset_error=fr->file_size; fr->offset_error=fr->file_size;
@ -174,6 +178,7 @@ static void file_check_nk2(file_recovery_t *fr)
{ {
char buf_entry_size[sizeof(uint32_t)]; char buf_entry_size[sizeof(uint32_t)];
const uint32_t *entry_size=(const uint32_t *)&buf_entry_size; const uint32_t *entry_size=(const uint32_t *)&buf_entry_size;
/*@ assert \valid_read(entry_size); */
if (fread(&buf_entry_size, sizeof(uint32_t), 1, fr->handle)!=1) if (fread(&buf_entry_size, sizeof(uint32_t), 1, fr->handle)!=1)
{ {
fr->offset_error=fr->file_size; fr->offset_error=fr->file_size;
@ -187,9 +192,11 @@ static void file_check_nk2(file_recovery_t *fr)
} }
break; break;
default: default:
#ifndef DISABLED_FOR_FRAMAC
log_info("nk2 entry %04x size=? at 0x%llx\n", log_info("nk2 entry %04x size=? at 0x%llx\n",
le16(entryh->value_type), le16(entryh->value_type),
(long long unsigned)fr->file_size); (long long unsigned)fr->file_size);
#endif
fr->offset_error=fr->file_size; fr->offset_error=fr->file_size;
fr->file_size=0; fr->file_size=0;
return; return;