diff --git a/src/Makefile.am b/src/Makefile.am
index 93aa68bf..10bfe689 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -389,7 +389,7 @@ file_C			= filegen.c \
 			  file_zip.c \
 			  file_zpr.c
 
-file_H			= ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_sp3.h file_tar.h file_tiff.h file_txt.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h
+file_H			= ext2.h hfsp_struct.h filegen.h file_doc.h file_jpg.h file_gz.h file_riff.h file_sp3.h file_tar.h file_tiff.h file_txt.h luks_struct.h ntfs_struct.h ole.h pe.h suspend.h
 
 photorec_C		= photorec.c phcfg.c addpart.c chgarch.c chgtype.c dir.c exfatp.c ext2grp.c ext2_dir.c ext2p.c fat_dir.c fatp.c file_found.c geometry.c ntfs_dir.c ntfsp.c pdisksel.c poptions.c sessionp.c dfxml.c partgptro.c
 
diff --git a/src/file_jpg.c b/src/file_jpg.c
index f37d5ca1..d603fadb 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -55,6 +55,9 @@
 #include "common.h"
 #include "log.h"
 #include "file_jpg.h"
+#if !defined(MAIN_jpg) && !defined(SINGLE_FORMAT)
+#include "file_riff.h"
+#endif
 #include "file_tiff.h"
 #include "setdate.h"
 #if defined(__FRAMAC__)
@@ -67,7 +70,6 @@ extern const file_hint_t file_hint_indd;
 extern const file_hint_t file_hint_mov;
 extern const file_hint_t file_hint_riff;
 extern const file_hint_t file_hint_rw2;
-extern data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
 #endif
 
 /*@ requires \valid(file_stat); */
diff --git a/src/file_riff.c b/src/file_riff.c
index 40b6d079..38e5bb07 100644
--- a/src/file_riff.c
+++ b/src/file_riff.c
@@ -31,11 +31,12 @@
 #include "types.h"
 #include "filegen.h"
 #include "common.h"
+#include "file_riff.h"
 #ifdef DEBUG_RIFF
 #include "log.h"
 #endif
 
-data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
+/*@ requires \valid(file_stat); */
 static void register_header_check_riff(file_stat_t *file_stat);
 
 const file_hint_t file_hint_riff= {
@@ -58,10 +59,10 @@ typedef struct {
   uint32_t dwSize;
   uint32_t dwFourCC;
 //  char data[dwSize-4];
-} riff_list_header;
+} riff_list_header_t;
 
 #ifdef DEBUG_RIFF
-static void log_riff_list(const uint64_t offset, const unsigned int depth, const riff_list_header *list_header)
+static void log_riff_list(const uint64_t offset, const unsigned int depth, const riff_list_header_t *list_header)
 {
   unsigned int i;
   log_info("0x%08lx - 0x%08lx ", offset, offset + 8 - 1 + le32(list_header->dwSize));
@@ -79,7 +80,7 @@ static void log_riff_list(const uint64_t offset, const unsigned int depth, const
       le32(list_header->dwSize));
 }
 
-static void log_riff_chunk(const uint64_t offset, const unsigned int depth, const riff_list_header *list_header)
+static void log_riff_chunk(const uint64_t offset, const unsigned int depth, const riff_list_header_t *list_header)
 {
   unsigned int i;
   if(le32(list_header->dwSize)==0)
@@ -96,53 +97,102 @@ static void log_riff_chunk(const uint64_t offset, const unsigned int depth, cons
 }
 #endif
 
+/*@
+  @ requires \valid(fr);
+  @ requires valid_file_recovery(fr);
+  @ requires \valid(fr->handle);
+  @ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
+  @ requires end <= PHOTOREC_MAX_FILE_SIZE;
+  @ ensures  valid_file_recovery(fr);
+  @ ensures  \valid(fr->handle);
+  @ assigns  *fr->handle, errno;
+  @ assigns  fr->offset_error;
+  @ assigns  Frama_C_entropy_source;
+  @*/
 static void check_riff_list(file_recovery_t *fr, const unsigned int depth, const uint64_t start, const uint64_t end)
 {
   uint64_t file_size;
-  riff_list_header list_header;
   if(depth>5)
     return;
+  /*@
+    @ loop invariant valid_file_recovery(fr);
+    @ loop invariant \valid(fr->handle);
+    @ loop assigns *fr->handle, errno;
+    @ loop assigns fr->offset_error;
+    @ loop assigns Frama_C_entropy_source;
+    @ loop assigns file_size;
+    @*/
   for(file_size=start; file_size < end;)
   {
+    char buf[sizeof(riff_list_header_t)];
+    uint64_t next_fs;
+    const riff_list_header_t *list_header=(const riff_list_header_t *)&buf;
     if(my_fseek(fr->handle, file_size, SEEK_SET)<0)
     {
       fr->offset_error=file_size;
       return;
     }
-    if (fread(&list_header, sizeof(list_header), 1, fr->handle)!=1)
+    if (fread(buf, sizeof(buf), 1, fr->handle)!=1)
     {
       fr->offset_error=file_size;
       return;
     }
-    if(memcmp(&list_header.dwList, "LIST", 4) == 0)
+#if defined(__FRAMAC__)
+    Frama_C_make_unknown(buf, sizeof(buf));
+#endif
+    /*@ assert \initialized((char *)list_header+ (0 .. sizeof(riff_list_header_t)-1)); */
+    next_fs=file_size + (uint64_t)8 + le32(list_header->dwSize);
+    if(next_fs > end)
+    {
+      fr->offset_error=file_size;
+      return;
+    }
+    /*@ assert valid_file_recovery(fr); */
+    if(memcmp(&list_header->dwList, "LIST", 4) == 0)
     {
 #ifdef DEBUG_RIFF
-      log_riff_list(file_size, depth, &list_header);
+      log_riff_list(file_size, depth, list_header);
 #endif
-      check_riff_list(fr, depth+1, file_size + sizeof(list_header), file_size + 8 - 1 + le32(list_header.dwSize));
+      check_riff_list(fr, depth+1, file_size + sizeof(riff_list_header_t), next_fs-1);
     }
     else
     {
 #ifdef DEBUG_RIFF
       /* It's a chunk */
-      log_riff_chunk(file_size, depth, &list_header);
+      log_riff_chunk(file_size, depth, list_header);
 #endif
     }
-    file_size += (uint64_t)8 + le32(list_header.dwSize);
+    file_size = next_fs;
     /* align to word boundary */
-    file_size += (file_size&1);
+    file_size = (file_size&1);
   }
 }
 
+/*@
+  @ requires \valid(fr);
+  @ requires valid_file_recovery(fr);
+  @ requires \separated(fr, fr->handle, fr->extension, &errno, &Frama_C_entropy_source);
+  @ requires fr->file_check == &file_check_avi;
+  @ ensures \valid(fr->handle);
+  @ assigns *fr->handle, errno, fr->file_size;
+  @ assigns fr->offset_error, fr->offset_ok;
+  @ assigns Frama_C_entropy_source;
+  @*/
 static void file_check_avi(file_recovery_t *fr)
 {
   fr->file_size = 0;
   fr->offset_error=0;
   fr->offset_ok=0;
+  /*@
+    @ loop assigns *fr->handle, errno, fr->file_size;
+    @ loop assigns fr->offset_error, fr->offset_ok;
+    @ loop assigns Frama_C_entropy_source;
+    @*/
   while(fr->file_size!=fr->calculated_file_size)
   {
     const uint64_t file_size=fr->file_size;
-    riff_list_header list_header;
+    riff_list_header_t list_header;
+    uint64_t calculated_file_size;
     if(my_fseek(fr->handle, fr->file_size, SEEK_SET)<0)
     {
       fr->file_size=0;
@@ -161,22 +211,42 @@ static void file_check_avi(file_recovery_t *fr)
       fr->offset_error=fr->file_size;
       return;
     }
-    check_riff_list(fr, 1, file_size + sizeof(list_header), file_size + 8 - 1 + le32(list_header.dwSize));
+    calculated_file_size=file_size + 8 + le32(list_header.dwSize);
+    if(calculated_file_size > PHOTOREC_MAX_FILE_SIZE)
+    {
+      fr->file_size=0;
+      return;
+    }
+    /*@ assert calculated_file_size <= PHOTOREC_MAX_FILE_SIZE; */
+    check_riff_list(fr, 1, file_size + sizeof(list_header), calculated_file_size - 1);
     if(fr->offset_error > 0)
     {
       fr->file_size=0;
       return;
     }
-    fr->file_size=file_size + 8 + le32(list_header.dwSize);
+    fr->file_size=calculated_file_size;
   }
 }
 
+/*@
+  @ requires buffer_size > 0;
+  @ requires (buffer_size&1)==0;
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires \valid(file_recovery);
+  @ requires file_recovery->data_check==&data_check_avi;
+  @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE;
+  @ requires \separated(buffer, file_recovery);
+  @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+  @ assigns file_recovery->calculated_file_size;
+  @*/
 static data_check_t data_check_avi(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
 {
+  /*@ loop assigns file_recovery->calculated_file_size; */
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
-      file_recovery->calculated_file_size + 12 < file_recovery->file_size + buffer_size/2)
+      file_recovery->calculated_file_size + 12 <= 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;
+    /*@ assert 0 <= i <= buffer_size - 12; */
     const riff_chunk_header *chunk_header=(const riff_chunk_header*)&buffer[i];
     if(memcmp(&buffer[i], "RIFF", 4)==0 && memcmp(&buffer[i+8], "AVIX", 4)==0)
       file_recovery->calculated_file_size += (uint64_t)8 + le32(chunk_header->dwSize);
@@ -188,10 +258,12 @@ static data_check_t data_check_avi(const unsigned char *buffer, const unsigned i
 
 data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
 {
+  /*@ loop assigns file_recovery->calculated_file_size; */
   while(file_recovery->calculated_file_size + buffer_size/2  >= file_recovery->file_size &&
-      file_recovery->calculated_file_size + 8 < file_recovery->file_size + buffer_size/2)
+      file_recovery->calculated_file_size + 8 <= 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;
+    /*@ assert 0 <= i <= buffer_size - 8; */
     const riff_chunk_header *chunk_header=(const riff_chunk_header*)&buffer[i];
     if(buffer[i+2]!='d' || buffer[i+3]!='b')	/* Video Data Binary ?*/
     {
@@ -208,12 +280,16 @@ data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned i
   return DC_CONTINUE;
 }
 
-static void file_check_size_rifx(file_recovery_t *file_recovery)
-{
-  if(file_recovery->file_size<file_recovery->calculated_file_size)
-    file_recovery->file_size=0;
-}
-
+/*@
+  @ requires buffer_size >= 12;
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_riff, buffer+(..), file_recovery, file_recovery_new);
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @*/
 static int header_check_riff(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)
 {
   uint64_t size;
@@ -252,7 +328,7 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
   size+=8;
   if(memcmp(&buffer[8],"AVI ",4)==0)
   {
-    const riff_list_header list_movi={
+    const riff_list_header_t list_movi={
       .dwList=be32(0x4c495354),	/* LIST */
       .dwSize=le32(4),
       .dwFourCC=be32(0x6d6f7669)	/* movi */
@@ -260,7 +336,7 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
     reset_file_recovery(file_recovery_new);
     file_recovery_new->extension="avi";
     /* Is it a raw avi stream with Data Binary chunks ? */
-    if(size < buffer_size - 4 &&
+    if(size >= sizeof(list_movi) && size <= buffer_size - 4 &&
 	memcmp(&buffer[size - sizeof(list_movi)], &list_movi, sizeof(list_movi)) ==0 &&
 	buffer[size+2]=='d' &&
 	buffer[size+3]=='b')
@@ -315,13 +391,23 @@ static int header_check_riff(const unsigned char *buffer, const unsigned int buf
   return 1;
 }
 
+/*@
+  @ requires buffer_size >= 12;
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires valid_file_recovery(file_recovery);
+  @ requires \valid(file_recovery_new);
+  @ requires file_recovery_new->blocksize > 0;
+  @ requires separation: \separated(&file_hint_riff, buffer+(..), file_recovery, file_recovery_new);
+  @ ensures  \result!=0 ==> valid_file_recovery(file_recovery_new);
+  @ assigns  *file_recovery_new;
+  @*/
 static int header_check_rifx(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)
 {
   if(memcmp(&buffer[8],"Egg!",4)==0)
   {
     /* After Effects */
     reset_file_recovery(file_recovery_new);
-    file_recovery_new->file_check=&file_check_size_rifx;
+    file_recovery_new->file_check=&file_check_size_min;
     file_recovery_new->calculated_file_size=(uint64_t)buffer[7]+(((uint64_t)buffer[6])<<8)+(((uint64_t)buffer[5])<<16)+(((uint64_t)buffer[4])<<24)+8;
     file_recovery_new->extension="aep";
     return 1;
diff --git a/src/file_riff.h b/src/file_riff.h
new file mode 100644
index 00000000..b0aa48d9
--- /dev/null
+++ b/src/file_riff.h
@@ -0,0 +1,44 @@
+/*
+
+    File: file_riff.h
+
+    Copyright (C) 2021 Christophe GRENIER <grenier@cgsecurity.org>
+
+    This software is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write the Free Software Foundation, Inc., 51
+    Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+ */
+#ifndef _FILE_RIFF_H
+#define _FILE_RIFF_H
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/*@
+  @ requires buffer_size > 0;
+  @ requires (buffer_size&1)==0;
+  @ requires \valid_read(buffer+(0..buffer_size-1));
+  @ requires \valid(file_recovery);
+  @ requires file_recovery->data_check==&data_check_avi_stream;
+  @ requires file_recovery->calculated_file_size <= PHOTOREC_MAX_FILE_SIZE;
+  @ requires \separated(buffer, file_recovery);
+  @ ensures \result == DC_CONTINUE || \result == DC_STOP;
+  @ assigns file_recovery->calculated_file_size;
+  @*/
+data_check_t data_check_avi_stream(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
+
+#ifdef __cplusplus
+} /* closing brace for extern "C" */
+#endif
+#endif