From ac2491463f3d9968408c7f39fbab2aa29cd0f260 Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sat, 10 Oct 2020 10:11:18 +0200
Subject: [PATCH] src/file_mpg.c: move frama-c annotation at the header
 definition

---
 src/file_mpg.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/file_mpg.c b/src/file_mpg.c
index c47cd211..ee27719c 100644
--- a/src/file_mpg.c
+++ b/src/file_mpg.c
@@ -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};