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

src/file_mpg.c: move frama-c annotation at the header definition

Browse source
This commit is contained in:
Christophe Grenier 2020-10-10 10:11:18 +02:00
parent f08ce6e528
commit ac2491463f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/file_mpg.c
View file

@ -33,6 +33,9 @@
#include "filegen.h"
#include "log.h"
/*@
@ requires \valid(file_stat);
@*/
static void register_header_check_mpg(file_stat_t *file_stat);
const file_hint_t file_hint_mpg= {
@ -397,9 +400,6 @@ static int header_check_mpg4_ElemVideo(const unsigned char *buffer, const unsign
return 0;
}
/*@
@ requires \valid(file_stat);
@*/
static void register_header_check_mpg(file_stat_t *file_stat)
{
static const unsigned char mpg_header_B3[4]= {0x00, 0x00, 0x01, 0xB3};