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

src/file_xm.c: fix Frama-C annotations

Browse source
This commit is contained in:
Christophe Grenier 2021-05-31 08:42:02 +02:00
parent ecd31c56da
commit 8f11e3a897
1 changed files with 15 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/file_xm.c
View file

@ -34,7 +34,7 @@
#include "filegen.h" #include "filegen.h"
#include "log.h" #include "log.h"
/*@ requires \valid(file_stat); */ /*@ requires valid_register_header_check(file_stat); */
static void register_header_check_xm(file_stat_t *file_stat); static void register_header_check_xm(file_stat_t *file_stat);
const file_hint_t file_hint_xm = { const file_hint_t file_hint_xm = {
@ -46,6 +46,12 @@ const file_hint_t file_hint_xm = {
.register_header_check = &register_header_check_xm .register_header_check = &register_header_check_xm
}; };
struct xm_hdr
{
uint16_t patterns;
uint16_t instrs;
} __attribute__ ((gcc_struct, __packed__));
/*@ /*@
@ requires \valid(fr); @ requires \valid(fr);
@ requires valid_file_recovery(fr); @ requires valid_file_recovery(fr);
@ -210,29 +216,27 @@ static int parse_instruments(file_recovery_t *fr, uint16_t instrs)
@ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source); @ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
@ requires fr->file_check == &file_check_xm; @ requires fr->file_check == &file_check_xm;
@ ensures \valid(fr->handle); @ ensures \valid(fr->handle);
@ assigns *fr->handle, errno, fr->file_size; @ assigns *fr->handle, fr->file_size, fr->offset_error;
@ assigns Frama_C_entropy_source; @ assigns Frama_C_entropy_source, errno;
@*/ @*/
static void file_check_xm(file_recovery_t *fr) static void file_check_xm(file_recovery_t *fr)
{ {
char buffer[4];
const struct xm_hdr *hdr=(const struct xm_hdr *)&buffer;
uint16_t patterns, instrs; uint16_t patterns, instrs;
fr->file_size = 0; fr->file_size = 0;
fr->offset_error = 0; fr->offset_error = 0;
fr->offset_ok = 0;
if(fseek(fr->handle, 70, SEEK_SET) == -1) if(fseek(fr->handle, 70, SEEK_SET) == -1)
return; return;
if(fread(&patterns, 2, 1, fr->handle) != 1) if(fread(&buffer, sizeof(buffer), 1, fr->handle) != 1)
return;
if(fread(&instrs, 2, 1, fr->handle) != 1)
return; return;
#if defined(__FRAMAC__) #if defined(__FRAMAC__)
Frama_C_make_unknown(&patterns, sizeof(patterns)); Frama_C_make_unknown(&buffer, sizeof(buffer));
Frama_C_make_unknown(&instrs, sizeof(instrs));
#endif #endif
instrs = le16(instrs); instrs = le16(hdr->instrs);
patterns = le16(patterns); patterns = le16(hdr->patterns);
#ifndef __FRAMAC__ #ifndef __FRAMAC__
log_debug("xm: %u patterns, %u instruments\n", patterns, instrs); log_debug("xm: %u patterns, %u instruments\n", patterns, instrs);