diff --git a/src/exfatp.c b/src/exfatp.c
index 00374ac3..06c24ec2 100644
--- a/src/exfatp.c
+++ b/src/exfatp.c
@@ -31,6 +31,7 @@
 #include "common.h"
 #include "list.h"
 #include "filegen.h"
+#include "photorec.h"
 #include "exfatp.h"
 #include "exfat.h"
 #include "log.h"
diff --git a/src/ext2p.c b/src/ext2p.c
index 84b2ca6f..6cbb0f7c 100644
--- a/src/ext2p.c
+++ b/src/ext2p.c
@@ -33,6 +33,7 @@
 #include "common.h"
 #include "list.h"
 #include "filegen.h"
+#include "photorec.h"
 #include "intrf.h"
 #include "dir.h"
 #ifdef HAVE_EXT2FS_EXT2_FS_H
diff --git a/src/fatp.c b/src/fatp.c
index af33ec3e..81fd62f0 100644
--- a/src/fatp.c
+++ b/src/fatp.c
@@ -31,6 +31,7 @@
 #include "common.h"
 #include "list.h"
 #include "filegen.h"
+#include "photorec.h"
 #include "fatp.h"
 #include "fat.h"
 #include "fat_common.h"
diff --git a/src/filegen.c b/src/filegen.c
index eb960cc5..8e909858 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -237,7 +237,12 @@ void file_search_footer(file_recovery_t *file_recovery, const void*footer, const
 }
 
 #if 0
-void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length)
+/*@
+  @ requires \valid(file_recovery);
+  @ requires footer_length > 0;
+  @ requires \valid_read((char *)footer+(0..footer_length-1));
+  @*/
+static void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length)
 {
   const unsigned int read_size=4096;
   unsigned char*buffer;
diff --git a/src/filegen.h b/src/filegen.h
index 2654443b..75f66b8f 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -139,18 +139,6 @@ uint64_t file_rsearch(FILE *handle, uint64_t offset, const void*footer, const un
   @*/
 void file_search_footer(file_recovery_t *file_recovery, const void*footer, const unsigned int footer_length, const unsigned int extra_length);
 
-/*@
-  @ requires \valid(file_recovery);
-  @ requires footer_length > 0;
-  @ requires \valid_read((char *)footer+(0..footer_length-1));
-  @*/
-void file_search_lc_footer(file_recovery_t *file_recovery, const unsigned char*footer, const unsigned int footer_length);
-
-/*@
-  @ requires \valid(list_search_space);
-  @*/
-void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end);
-
 /*@
   @ requires buffer_size > 0;
   @ requires \valid_read((char *)buffer+(0..buffer_size-1));
diff --git a/src/ntfsp.c b/src/ntfsp.c
index 6da68227..b6a040ae 100644
--- a/src/ntfsp.c
+++ b/src/ntfsp.c
@@ -37,6 +37,7 @@
 #include "common.h"
 #include "list.h"
 #include "filegen.h"
+#include "photorec.h"
 #ifdef HAVE_LIBNTFS
 #include <ntfs/attrib.h>
 #endif
diff --git a/src/photorec.c b/src/photorec.c
index f98ee433..c84d54c9 100644
--- a/src/photorec.c
+++ b/src/photorec.c
@@ -85,6 +85,11 @@ void del_search_space(alloc_data_t *list_search_space, const uint64_t start, con
   update_search_space_aux(list_search_space, start, end, NULL, NULL);
 }
 
+/*@
+  @ requires \valid(list_search_space);
+  @ requires new_current_search_space == \null || \valid(*new_current_search_space);
+  @ requires offset == \null || \valid(*offset);
+  @*/
 static void update_search_space_aux(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end, alloc_data_t **new_current_search_space, uint64_t *offset)
 {
   struct td_list_head *search_walker = NULL;
diff --git a/src/photorec.h b/src/photorec.h
index 4aa30e0f..ed1c08df 100644
--- a/src/photorec.h
+++ b/src/photorec.h
@@ -93,6 +93,12 @@ void file_block_log(const file_recovery_t *file_recovery, const unsigned int sec
 void file_block_free(alloc_list_t *list_allocation);
 void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search_space, alloc_data_t **new_current_search_space, uint64_t *offset, const unsigned int blocksize, const unsigned int data);
 void file_block_truncate_and_move(file_recovery_t *file_recovery, alloc_data_t *list_search_space, const unsigned int blocksize,  alloc_data_t **new_current_search_space, uint64_t *offset, unsigned char *buffer);
+
+/*@
+  @ requires \valid(list_search_space);
+  @*/
+void del_search_space(alloc_data_t *list_search_space, const uint64_t start, const uint64_t end);
+
 #ifdef __cplusplus
 } /* closing brace for extern "C" */
 #endif