diff --git a/src/file_mpg.c b/src/file_mpg.c
index ee27719c..f911cf0e 100644
--- a/src/file_mpg.c
+++ b/src/file_mpg.c
@@ -160,7 +160,7 @@ static data_check_t data_check_mpg(const unsigned char *buffer, const unsigned i
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
       file_recovery->calculated_file_size + 14 < file_recovery->file_size + buffer_size/2)
   {
-    const unsigned int i=file_recovery->calculated_file_size - file_recovery->file_size + buffer_size/2;
+    const unsigned int i=file_recovery->calculated_file_size + buffer_size/2 - file_recovery->file_size;
     const unsigned int ret=calculate_packet_size(&buffer[i]);
 #ifdef DEBUG_MPG
     log_info("data_check_mpg %llu 0x%02x %u\n", (long long unsigned)file_recovery->calculated_file_size, buffer[i+3], ret);
@@ -172,6 +172,11 @@ static data_check_t data_check_mpg(const unsigned char *buffer, const unsigned i
   return DC_CONTINUE;
 }
 
+/*@
+  @ requires \valid(file_recovery_new);
+  @ ensures  valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @*/
 static int header_mpg_found(file_recovery_t *file_recovery_new)
 {
   reset_file_recovery(file_recovery_new);
@@ -183,6 +188,28 @@ static int header_mpg_found(file_recovery_t *file_recovery_new)
   return 1;
 }
 
+/*@
+  @ requires buffer_size >= 13;
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ assigns \nothing;
+  @*/
+static int is_valid_packet_size(const unsigned char *buffer, const unsigned int buffer_size)
+{
+  unsigned int i=0;
+  /*@
+    @ loop assigns i;
+    @*/
+  while(i+14 < td_min(buffer_size,512U))
+  {
+    /*@ assert i < buffer_size - 14; */
+    const unsigned int ret=calculate_packet_size(&buffer[i]);
+    if(ret==0)
+      return 0;
+    i+=ret;
+  }
+  return 1;
+}
+
 /*@
   @ requires buffer_size >= 13;
   @ requires \valid_read(buffer+(0..buffer_size-1));
@@ -194,17 +221,8 @@ static int header_mpg_found(file_recovery_t *file_recovery_new)
   @*/
 static int header_check_mpg_Pack(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)
 {
-  unsigned int i=0;
-  /*@
-    @ loop assigns i;
-    @*/
-  while(i+14 < td_min(buffer_size,512U))
-  {
-    const unsigned int ret=calculate_packet_size(&buffer[i]);
-    if(ret==0)
-      return 0;
-    i+=ret;
-  }
+  if(is_valid_packet_size(buffer, buffer_size)==0)
+    return 0;
   /* MPEG-1 http://andrewduncan.ws/MPEG/MPEG-1.ps */
   /* pack start code 0x1BA + MPEG-1 + SCR=0 */
   if((buffer[4]&0xF1)==0x21 && (buffer[6]&1)==1 && (buffer[8]&1)==1 &&
@@ -290,17 +308,8 @@ static int header_check_mpg_System(const unsigned char *buffer, const unsigned i
   /* MPEG-1 system header start code */
   if((buffer[6]&0x80)==0x80 && (buffer[8]&0x01)==0x01 && buffer[11]==0xff)
   {
-    unsigned int i=0;
-    /*@
-      @ loop assigns i;
-      @*/
-    while(i+14 < td_min(buffer_size,512U))
-    {
-      const unsigned int ret=calculate_packet_size(&buffer[i]);
-      if(ret==0)
-	return 0;
-      i+=ret;
-    }
+    if(is_valid_packet_size(buffer, buffer_size)==0)
+      return 0;
     if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_mpg)
     {
       header_ignored(file_recovery_new);
@@ -336,17 +345,8 @@ static int header_check_mpg_Sequence(const unsigned char *buffer, const unsigned
       /* marker */
       (buffer[10]&0x20)==0x20)
   {
-    unsigned int i=0;
-    /*@
-      @ loop assigns i;
-      @*/
-    while(i+14 < td_min(buffer_size,512U))
-    {
-      const unsigned int ret=calculate_packet_size(&buffer[i]);
-      if(ret==0)
-	return 0;
-      i+=ret;
-    }
+    if(is_valid_packet_size(buffer, buffer_size)==0)
+      return 0;
     if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_mpg)
     {
       header_ignored(file_recovery_new);
@@ -379,17 +379,8 @@ static int header_check_mpg4_ElemVideo(const unsigned char *buffer, const unsign
       (buffer[5]>>4)!=0 && (buffer[5]>>4)!=0x0f
     )
   {
-    unsigned int i=0;
-    /*@
-      @ loop assigns i;
-      @*/
-    while(i+14 < td_min(buffer_size,512U))
-    {
-      const unsigned int ret=calculate_packet_size(&buffer[i]);
-      if(ret==0)
-	return 0;
-      i+=ret;
-    }
+    if(is_valid_packet_size(buffer, buffer_size)==0)
+      return 0;
     if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_mpg)
     {
       header_ignored(file_recovery_new);