diff --git a/src/alignio.h b/src/alignio.h
index be949e26..cc4d6b0f 100644
--- a/src/alignio.h
+++ b/src/alignio.h
@@ -33,6 +33,7 @@
   @ requires offset < 0x8000000000000000;
   @ requires \valid((char *)buf + (0 .. count -1));
   @ requires \separated(disk_car, (char *)buf);
+  @ decreases 0;
   @ ensures  valid_disk(disk_car);
   @*/
 static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset),
@@ -90,6 +91,7 @@ static int align_pread(int (*fnct_pread)(const disk_t *disk_car, void *buf, cons
   @ requires offset < 0x8000000000000000;
   @ requires \valid_read((char *)buf + (0 .. count -1));
   @ requires \separated(disk_car, (char *)buf);
+  @ decreases 0;
   @ ensures  valid_disk(disk_car);
   @*/
 static int align_pwrite(int (*fnct_pread)(const disk_t *disk_car, void *buf, const unsigned int count, const uint64_t offset),
diff --git a/src/analyse.h b/src/analyse.h
index 6b3f3836..047ccbb6 100644
--- a/src/analyse.h
+++ b/src/analyse.h
@@ -31,6 +31,7 @@ extern "C" {
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_0(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -40,6 +41,7 @@ int search_type_0(const unsigned char *buffer, disk_t *disk_car,partition_t *par
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_1(const unsigned char *buffer, const disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind);
 
@@ -49,6 +51,7 @@ int search_type_1(const unsigned char *buffer, const disk_t *disk_car, partition
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_2(const unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -58,6 +61,7 @@ int search_type_2(const unsigned char *buffer, disk_t *disk_car,partition_t *par
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_8(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -67,6 +71,7 @@ int search_type_8(unsigned char *buffer, disk_t *disk_car,partition_t *partition
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_16(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -76,6 +81,7 @@ int search_type_16(unsigned char *buffer, disk_t *disk_car,partition_t *partitio
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_64(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -85,6 +91,7 @@ int search_type_64(unsigned char *buffer, disk_t *disk_car,partition_t *partitio
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_128(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -94,6 +101,7 @@ int search_type_128(unsigned char *buffer, disk_t *disk_car,partition_t *partiti
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_type_2048(unsigned char *buffer, disk_t *disk_car,partition_t *partition,const int verbose, const int dump_ind);
 
@@ -103,6 +111,7 @@ int search_type_2048(unsigned char *buffer, disk_t *disk_car,partition_t *partit
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk, partition);
+  @ decreases 0;
   @*/
 int search_exFAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partition);
 
@@ -112,6 +121,7 @@ int search_exFAT_backup(unsigned char *buffer, disk_t *disk, partition_t *partit
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_FAT_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
 
@@ -121,6 +131,7 @@ int search_FAT_backup(unsigned char *buffer, disk_t *disk_car,partition_t *parti
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_HFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
 
@@ -130,6 +141,7 @@ int search_HFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *parti
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \separated(buffer, disk_car, partition);
+  @ decreases 0;
   @*/
 int search_NTFS_backup(unsigned char *buffer, disk_t *disk_car,partition_t *partition, const int verbose, const int dump_ind);
 
diff --git a/src/apfs.h b/src/apfs.h
index b9163c4f..a9932e88 100644
--- a/src/apfs.h
+++ b/src/apfs.h
@@ -30,6 +30,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_APFS(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/bfs.h b/src/bfs.h
index fb3dd7d0..d1a3b0d9 100644
--- a/src/bfs.h
+++ b/src/bfs.h
@@ -90,6 +90,7 @@ struct disk_super_block          /* super block as it is on disk */
   @ requires \valid(partition);
   @ requires valid_disk(disk_car);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_BeFS(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/bsd.h b/src/bsd.h
index 52c9f02c..82c4746d 100644
--- a/src/bsd.h
+++ b/src/bsd.h
@@ -174,6 +174,7 @@ struct disklabel {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_BSD(disk_t *disk_car, partition_t *partition, const int verbose, const unsigned int max_partitions);
 
diff --git a/src/btrfs.h b/src/btrfs.h
index 022c6962..d916f593 100644
--- a/src/btrfs.h
+++ b/src/btrfs.h
@@ -145,6 +145,7 @@ struct btrfs_super_block {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_btrfs(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/chgtype.h b/src/chgtype.h
index 3365eb51..3308a0d5 100644
--- a/src/chgtype.h
+++ b/src/chgtype.h
@@ -32,6 +32,7 @@ extern "C" {
   @ requires valid_partition(partition);
   @ requires \valid(current_cmd);
   @ requires \separated(disk_car, partition, current_cmd);
+  @ decreases 0;
   @*/
 void change_part_type_cli(const disk_t *disk_car,partition_t *partition, char **current_cmd);
 
diff --git a/src/cramfs.h b/src/cramfs.h
index eef22aae..695f4072 100644
--- a/src/cramfs.h
+++ b/src/cramfs.h
@@ -89,6 +89,7 @@ struct cramfs_super {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_cramfs(disk_t *disk_car,partition_t *partition,const int verbose);
 
diff --git a/src/exfat.h b/src/exfat.h
index 29e0eee1..54ae4d80 100644
--- a/src/exfat.h
+++ b/src/exfat.h
@@ -106,6 +106,7 @@ uint64_t exfat_cluster_to_offset(const struct exfat_super_block *exfat_header, c
   @ requires \valid_read(partition);
   @ requires \valid_read(exfat_header);
   @ requires \separated(disk, partition, exfat_header, (char *)buffer);
+  @ decreases 0;
   @*/
 int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct exfat_super_block*exfat_header, void *buffer, const unsigned int cluster);
 
@@ -114,6 +115,7 @@ int exfat_read_cluster(disk_t *disk, const partition_t *partition, const struct
   @ requires valid_disk(disk);
   @ requires \valid(partition);
   @ requires \separated(disk, partition);
+  @ decreases 0;
   @*/
 int check_exFAT(disk_t *disk, partition_t *partition);
 
diff --git a/src/exfatp.h b/src/exfatp.h
index f31d323a..f14d28ac 100644
--- a/src/exfatp.h
+++ b/src/exfatp.h
@@ -32,6 +32,7 @@ extern "C" {
   @ requires valid_partition(partition);
   @ requires valid_list_search_space(list_search_space);
   @ requires \separated(disk, partition, list_search_space);
+  @ decreases 0;
   @*/
 // ensures  valid_list_search_space(list_search_space);
 unsigned int exfat_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space);
diff --git a/src/ext2.h b/src/ext2.h
index bee4d595..dbf8ed8e 100644
--- a/src/ext2.h
+++ b/src/ext2.h
@@ -30,6 +30,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_EXT2(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/ext2grp.h b/src/ext2grp.h
index 231db84d..96f4f886 100644
--- a/src/ext2grp.h
+++ b/src/ext2grp.h
@@ -32,6 +32,7 @@ extern "C" {
   @ requires \valid(disk);
   @ requires \valid_read(partition);
   @ requires \separated(list_search_space, disk, partition);
+  @ decreases 0;
   @ ensures  valid_disk(disk);
   @*/
 // ensures  valid_list_search_space(list_search_space);
@@ -45,6 +46,7 @@ unsigned int ext2_fix_group(alloc_data_t *list_search_space, disk_t *disk, const
   @ requires \valid(disk);
   @ requires \valid_read(partition);
   @ requires \separated(list_search_space, disk, partition);
+  @ decreases 0;
   @ ensures  valid_disk(disk);
   @*/
 // ensures  valid_list_search_space(list_search_space);
diff --git a/src/f2fs.h b/src/f2fs.h
index 46949bfd..312799a7 100644
--- a/src/f2fs.h
+++ b/src/f2fs.h
@@ -30,6 +30,7 @@ extern "C" {
   @ requires valid_disk(disk);
   @ requires \valid(partition);
   @ requires \separated(disk, partition);
+  @ decreases 0;
   @*/
 int check_f2fs(disk_t *disk, partition_t *partition);
 
diff --git a/src/fat.h b/src/fat.h
index 04603de7..61924bac 100644
--- a/src/fat.h
+++ b/src/fat.h
@@ -33,6 +33,7 @@ extern "C" {
   @ requires \valid_read(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 int comp_FAT(disk_t *disk, const partition_t *partition, const unsigned long int fat_size, const unsigned long int sect_res);
 
@@ -57,6 +58,7 @@ unsigned int get_next_cluster(disk_t *disk, const partition_t *partition, const
   @ requires \valid_read(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 int set_next_cluster(disk_t *disk, const partition_t *partition, const upart_type_t upart_type, const int offset, const unsigned int cluster, const unsigned int next_cluster);
 
@@ -96,6 +98,7 @@ int is_part_fat32(const partition_t *partition);
   @ requires \valid_read(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int cluster, const unsigned int no_of_cluster);
 
@@ -107,6 +110,7 @@ unsigned int fat32_get_prev_cluster(disk_t *disk, const partition_t *partition,
   @ requires separation: \separated(disk, partition);
   @ requires \valid(next_free);
   @ requires \valid(free_count);
+  @ decreases 0;
   @*/
 int fat32_free_info(disk_t *disk, const partition_t *partition, const unsigned int fat_offset, const unsigned int no_of_cluster, unsigned int *next_free, unsigned int *free_count);
 
@@ -138,6 +142,7 @@ int recover_FAT(disk_t *disk, const struct fat_boot_sector*fat_header, partition
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 int check_FAT(disk_t *disk, partition_t *partition, const int verbose);
 
@@ -167,6 +172,7 @@ int recover_OS2MB(const disk_t *disk, const struct fat_boot_sector*fat_header, p
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 int check_OS2MB(disk_t *disk, partition_t *partition, const int verbose);
 
diff --git a/src/fat_cluster.h b/src/fat_cluster.h
index df818a66..aeb3bba8 100644
--- a/src/fat_cluster.h
+++ b/src/fat_cluster.h
@@ -50,6 +50,7 @@ struct cluster_offset_struct
   @ requires \valid(sectors_per_cluster);
   @ requires \valid(offset);
   @ requires \separated(disk_car, partition, sectors_per_cluster, offset);
+  @ decreases 0;
   @*/
 int find_sectors_per_cluster(disk_t *disk_car, const partition_t *partition, const int verbose, const int dump_ind, unsigned int *sectors_per_cluster, uint64_t *offset, const upart_type_t upart_type);
 
diff --git a/src/fat_dir.h b/src/fat_dir.h
index 9e1d34a5..8028500d 100644
--- a/src/fat_dir.h
+++ b/src/fat_dir.h
@@ -41,6 +41,7 @@ int dir_fat_aux(const unsigned char*buffer, const unsigned int size, const unsig
   @ requires valid_partition(partition);
   @ requires \valid(dir_data);
   @ requires \separated(disk_car, partition, dir_data);
+  @ decreases 0;
   @*/
 dir_partition_t dir_partition_fat_init(disk_t *disk_car, const partition_t *partition, dir_data_t *dir_data, const int verbose);
 
diff --git a/src/fatp.c b/src/fatp.c
index a227082e..a98f13a6 100644
--- a/src/fatp.c
+++ b/src/fatp.c
@@ -44,6 +44,7 @@
   @ requires valid_partition(partition);
   @ requires \valid(list_search_space);
   @ requires \separated(disk, partition, list_search_space);
+  @ decreases 0;
   @*/
 static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
@@ -101,6 +102,7 @@ static void fat12_remove_used_space(disk_t *disk,const partition_t *partition, a
   @ requires valid_partition(partition);
   @ requires \valid(list_search_space);
   @ requires \separated(disk_car, partition, list_search_space);
+  @ decreases 0;
   @*/
 static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
@@ -153,6 +155,7 @@ static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partitio
   @ requires valid_partition(partition);
   @ requires \valid(list_search_space);
   @ requires \separated(disk_car, partition, list_search_space);
+  @ decreases 0;
   @*/
 static void fat32_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
 {
diff --git a/src/fatp.h b/src/fatp.h
index 699a25e3..745ee827 100644
--- a/src/fatp.h
+++ b/src/fatp.h
@@ -32,6 +32,7 @@ extern "C" {
   @ requires valid_partition(partition);
   @ requires valid_list_search_space(list_search_space);
   @ requires \separated(disk_car, partition, list_search_space);
+  @ decreases 0;
   @*/
 // ensures  valid_list_search_space(list_search_space);
 unsigned int fat_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space);
diff --git a/src/filegen.h b/src/filegen.h
index 4fbbcf5f..2051b882 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -356,6 +356,7 @@ void register_header_check(const unsigned int offset, const void *value, const u
 
 /*@
   @ requires \valid(files_enable);
+  @ decreases 0;
   @*/
 file_stat_t * init_file_stats(file_enable_t *files_enable);
 
@@ -393,6 +394,7 @@ void header_ignored(const file_recovery_t *file_recovery_new);
   @ requires \valid_function(file_recovery->file_check);
   @ requires \initialized(&file_recovery->file_check);
   @ requires \initialized(&file_recovery->handle);
+  @ decreases 0;
   @ ensures \result == 0 || \result == 1;
   @*/
 // ensures  valid_file_recovery(file_recovery);
diff --git a/src/gfs2.h b/src/gfs2.h
index b3a7af05..9d0941bf 100644
--- a/src/gfs2.h
+++ b/src/gfs2.h
@@ -84,6 +84,7 @@ struct gfs2_sb {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_gfs2(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/hdaccess.h b/src/hdaccess.h
index 81d1c011..6cd2938f 100644
--- a/src/hdaccess.h
+++ b/src/hdaccess.h
@@ -30,12 +30,13 @@ extern "C" {
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.heads_per_cylinder > 0;
   @ requires \valid_function(disk_car->pread);
+  @ decreases 0;
   @ ensures  valid_disk(disk_car);
   @*/
 void hd_update_geometry(disk_t *disk_car, const int verbose);
 
 /*@
-  @ requires list_disk==\null || \valid_read(list_disk);
+  @ requires valid_list_disk(list_disk);
   @*/
 void hd_update_all_geometry(const list_disk_t * list_disk, const int verbose);
 
@@ -47,11 +48,10 @@ list_disk_t *hd_parse(list_disk_t *list_disk, const int verbose, const int testd
 
 /*@
   @ requires valid_read_string(device);
-  @ ensures  valid_disk(\result);
   @ ensures  \result!=\null ==> (0 < \result->geom.cylinders < 0x2000000000000);
   @ ensures  \result!=\null ==> (0 < \result->geom.heads_per_cylinder <= 255);
   @ ensures  \result!=\null ==> (0 < \result->geom.sectors_per_head <= 63);
-  @ ensures  valid_disk(\result);
+  @ ensures  \result==\null || valid_disk(\result);
   @*/
 disk_t *file_test_availability(const char *device, const int verbose, const int testdisk_mode);
 
diff --git a/src/hfs.h b/src/hfs.h
index cc500d2f..6448fe1e 100644
--- a/src/hfs.h
+++ b/src/hfs.h
@@ -81,6 +81,7 @@ struct hfs_mdb {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_HFS(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/hfsp.h b/src/hfsp.h
index a961904b..d42543ad 100644
--- a/src/hfsp.h
+++ b/src/hfsp.h
@@ -30,6 +30,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_HFSP(disk_t *disk_car, partition_t *partition, const int verbose);
 
@@ -48,6 +49,7 @@ int test_HFSP(const disk_t *disk_car, const struct hfsp_vh *vh, const partition_
   @ requires \valid_read(vh);
   @ requires \valid(partition);
   @ requires \separated(disk_car, vh, partition);
+  @ decreases 0;
   @*/
 int recover_HFSP(disk_t *disk_car, const struct hfsp_vh *vh, partition_t *partition, const int verbose, const int dump_ind, const int backup);
 
diff --git a/src/hpfs.h b/src/hpfs.h
index 0e950801..bbcc0c45 100644
--- a/src/hpfs.h
+++ b/src/hpfs.h
@@ -40,6 +40,7 @@ int recover_HPFS(const disk_t *disk_car, const struct fat_boot_sector *hpfs_head
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_HPFS(disk_t *disk_car,partition_t *partition, const int verbose);
 
diff --git a/src/io_redir.c b/src/io_redir.c
index 5fa867a9..9b09af7c 100644
--- a/src/io_redir.c
+++ b/src/io_redir.c
@@ -60,12 +60,14 @@ struct info_io_redir
   @ requires valid_disk(disk_car);
   @ requires \valid((char *)buffer + (0 .. count-1));
   @ requires separation: \separated(disk_car, (char *)buffer + (0 .. count-1));
+  @ decreases 0;
   @*/
 static int io_redir_pread(disk_t *disk_car, void *buffer, const unsigned int count, const uint64_t offset);
 
 /*@
   @ requires \valid(disk_car);
   @ requires valid_disk(disk_car);
+  @ decreases 0;
   @*/
 static void io_redir_clean(disk_t *disk_car);
 
diff --git a/src/iso.h b/src/iso.h
index bd3e94ff..63de0017 100644
--- a/src/iso.h
+++ b/src/iso.h
@@ -31,6 +31,7 @@ extern "C" {
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_ISO(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/jfs.h b/src/jfs.h
index 55967025..273c2a7a 100644
--- a/src/jfs.h
+++ b/src/jfs.h
@@ -33,6 +33,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_JFS(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/list_sort.c b/src/list_sort.c
index 92318a51..1edd7fb8 100644
--- a/src/list_sort.c
+++ b/src/list_sort.c
@@ -36,6 +36,9 @@
  * to chaining of merge() calls: null-terminated, no reserved or
  * sentinel head node, "prev" links not maintained.
  */
+/*@
+  @ decreases 0;
+  @*/
 static struct td_list_head *merge(
     int (*cmp)(const struct td_list_head *a, const struct td_list_head *b),
     struct td_list_head *a, struct td_list_head *b)
@@ -64,6 +67,9 @@ static struct td_list_head *merge(
  * prev-link restoration pass, or maintaining the prev links
  * throughout.
  */
+/*@
+  @ decreases 0;
+  @*/
 static void merge_and_restore_back_links(
     int (*cmp)(const struct td_list_head *a, const struct td_list_head *b),
     struct td_list_head *head,
diff --git a/src/luks.h b/src/luks.h
index f10c5afb..520721a3 100644
--- a/src/luks.h
+++ b/src/luks.h
@@ -32,6 +32,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_LUKS(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/netware.h b/src/netware.h
index 67b2c4d4..7c31aec8 100644
--- a/src/netware.h
+++ b/src/netware.h
@@ -39,6 +39,7 @@ struct disk_netware
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_netware(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/ntfs.c b/src/ntfs.c
index ec2c8f64..22cb4f16 100644
--- a/src/ntfs.c
+++ b/src/ntfs.c
@@ -43,10 +43,30 @@
 #include "fnctdsk.h"
 #include "lang.h"
 #include "log.h"
-/* #include "guid_cmp.h" */
-extern const arch_fnct_t arch_i386;
 
+#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
+extern const arch_fnct_t arch_i386;
+#endif
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(ntfs_header);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \separated(disk_car, ntfs_header, partition);
+  @*/
 static void set_NTFS_info(disk_t *disk_car, const struct ntfs_boot_sector*ntfs_header, partition_t *partition);
+
+/*@
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid(partition);
+  @ requires valid_partition(partition);
+  @ requires \valid_read(ntfs_header);
+  @ requires \separated(disk_car, partition, ntfs_header);
+  @ decreases 0;
+  @*/
 static void ntfs_get_volume_name(disk_t *disk_car, partition_t *partition, const struct ntfs_boot_sector*ntfs_header);
 
 unsigned int ntfs_sector_size(const struct ntfs_boot_sector *ntfs_header)
@@ -369,6 +389,7 @@ static void ntfs_get_volume_name(disk_t *disk_car, partition_t *partition, const
 
 int is_part_ntfs(const partition_t *partition)
 {
+#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_I386)
   if(partition->arch==&arch_i386)
   {
     switch(partition->part_type_i386)
@@ -380,13 +401,7 @@ int is_part_ntfs(const partition_t *partition)
         break;
     }
   }
-  /*
-  else if(partition->arch==&arch_gpt)
-  {
-    if(guid_cmp(partition->part_type_gpt,GPT_ENT_TYPE_MS_BASIC_DATA)==0)
-      return 1;
-  }
-  */
+#endif
   return 0;
 }
 
diff --git a/src/ntfs.h b/src/ntfs.h
index 9a42ba2b..c1b5a243 100644
--- a/src/ntfs.h
+++ b/src/ntfs.h
@@ -31,6 +31,7 @@ extern "C" {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_NTFS(disk_t *disk_car, partition_t *partition, const int verbose, const int dump_ind);
 
diff --git a/src/partauto.h b/src/partauto.h
index dbd7d7bc..1929c69b 100644
--- a/src/partauto.h
+++ b/src/partauto.h
@@ -31,6 +31,7 @@ extern "C" {
   @ requires \valid_read(arch);
   @ requires valid_disk(disk);
   @ requires separation: \separated(disk, arch);
+  @ decreases 0;
   @ ensures  valid_disk(disk);
   @*/
 void autodetect_arch(disk_t *disk, const arch_fnct_t *arch);
diff --git a/src/pdisksel.c b/src/pdisksel.c
index aa86ab25..8e06b567 100644
--- a/src/pdisksel.c
+++ b/src/pdisksel.c
@@ -41,7 +41,7 @@ disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *l
   const list_disk_t *element_disk;
   disk_t *disk=NULL;
   /*@
-    @ loop invariant valid_disk(disk);
+    @ loop invariant disk==\null || valid_disk(disk);
     @ loop assigns element_disk, disk;
     @*/
   for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next)
@@ -51,6 +51,7 @@ disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *l
   }
   if(disk==NULL)
     return NULL;
+  /*@ assert valid_disk(disk); */
   {
     /* disk sector size is now known, fix the sector ranges */
     struct td_list_head *search_walker = NULL;
diff --git a/src/pdisksel.h b/src/pdisksel.h
index a03ce556..2daadb66 100644
--- a/src/pdisksel.h
+++ b/src/pdisksel.h
@@ -27,11 +27,10 @@ extern "C" {
 
 /*@
   @ requires valid_read_string(cmd_device);
-  @ requires \valid_read(list_disk);
-  @ requires valid_disk(list_disk->disk);
+  @ requires valid_list_disk(list_disk);
   @ requires \valid(list_search_space);
   @ requires \separated(cmd_device, list_disk, list_search_space);
-  @ ensures  valid_disk(\result);
+  @ ensures  \result==\null || valid_disk(\result);
   @*/
 disk_t *photorec_disk_selection_cli(const char *cmd_device, const list_disk_t *list_disk, alloc_data_t *list_search_space);
 
diff --git a/src/pdiskseln.h b/src/pdiskseln.h
index a961b470..9609edaa 100644
--- a/src/pdiskseln.h
+++ b/src/pdiskseln.h
@@ -29,7 +29,7 @@ extern "C" {
   @ requires \valid(params);
   @ requires valid_ph_param(params);
   @ requires \valid(options);
-  @ requires list_disk == \null || (\valid_read(list_disk) && valid_disk(list_disk->disk));
+  @ requires valid_list_disk(list_disk);
   @ requires params->cmd_device==\null || valid_read_string(params->cmd_device);
   @ requires params->cmd_run==\null || valid_read_string(params->cmd_run);
   @ requires params->disk==\null;
diff --git a/src/photorec.h b/src/photorec.h
index 84cbb503..517efdbe 100644
--- a/src/photorec.h
+++ b/src/photorec.h
@@ -225,6 +225,15 @@ uint64_t set_search_start(struct ph_param *params, alloc_data_t **new_current_se
   @ requires valid_ph_param(params);
   @ requires \valid_read(options);
   @ requires \separated(params, options);
+  @ requires params->disk->sector_size > 0;
+  @ requires valid_read_string(params->recup_dir);
+  @ ensures  valid_ph_param(params);
+  @ ensures  params->file_nbr == 0;
+  @ ensures  params->status == STATUS_FIND_OFFSET;
+  @ ensures  params->dir_num == 1;
+  @ ensures  params->offset == PH_INVALID_OFFSET;
+  @ ensures  params->blocksize > 0;
+  @ ensures  valid_read_string(params->recup_dir);
   @*/
 void params_reset(struct ph_param *params, const struct ph_options *options);
 
@@ -238,6 +247,7 @@ const char *status_to_name(const photorec_status_t status);
   @ requires valid_ph_param(params);
   @ requires \valid_read(options);
   @ requires \separated(params, options);
+  @ ensures  valid_ph_param(params);
   @ assigns  params->offset, params->status, params->file_nbr;
   @*/
 void status_inc(struct ph_param *params, const struct ph_options *options);
@@ -249,6 +259,7 @@ void status_inc(struct ph_param *params, const struct ph_options *options);
   @ requires \valid_function(disk->arch->read_part);
   @ requires \valid_read(options);
   @ requires \separated(disk, options);
+  @ decreases 0;
   @ ensures  valid_disk(disk);
   @*/
 // ensures  valid_list_part(\result);
@@ -276,6 +287,7 @@ void file_block_append(file_recovery_t *file_recovery, alloc_data_t *list_search
   @ requires valid_list_search_space(list_search_space);
   @ requires \separated(file_recovery, list_search_space, new_current_search_space, offset, buffer + (..));
   @ requires new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space));
+  @ decreases 0;
   @*/
 // ensures  new_current_search_space==\null || (\valid(*new_current_search_space) && valid_list_search_space(*new_current_search_space));
 // ensures  valid_file_recovery(file_recovery);
diff --git a/src/photorec_check_header.h b/src/photorec_check_header.h
index a13ba3ce..3b375e74 100644
--- a/src/photorec_check_header.h
+++ b/src/photorec_check_header.h
@@ -24,8 +24,12 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar)
 extern const file_hint_t file_hint_tar;
+#endif
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir)
 extern const file_hint_t file_hint_dir;
+#endif
 extern file_check_list_t file_check_list;
 
 #if defined(__CYGWIN__) || defined(__MINGW32__)
@@ -122,7 +126,7 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
 	(unsigned long)(file_recovery->location.start/params->disk->sector_size));
   }
 #endif
-#ifndef __FRAMAC__
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_dir)
   if(file_recovery->file_stat->file_hint==&file_hint_dir && options->verbose > 0)
   { /* FAT directory found, list the file */
     const unsigned int blocksize=params->blocksize;
@@ -160,6 +164,7 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
   @ requires \valid_read(buffer + (0 .. params->blocksize -1));
   @ requires \valid(file_recovered);
   @ requires \separated(file_recovery, params, options, list_search_space, buffer, file_recovered);
+  @ decreases 0;
   @ ensures  valid_file_recovery(file_recovery);
   @*/
 // ensures  valid_list_search_space(list_search_space);
@@ -172,6 +177,7 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st
   /*@ assert valid_file_recovery(file_recovery); */
   file_recovery_new.blocksize=blocksize;
   file_recovery_new.location.start=offset;
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tar)
   if(file_recovery->file_stat!=NULL && file_recovery->file_stat->file_hint==&file_hint_tar &&
       is_valid_tar_header((const struct tar_posix_header *)(buffer-0x200)))
   { /* Currently saving a tar, do not check the data for know header */
@@ -182,8 +188,10 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st
 	  (unsigned long)((offset-params->partition->part_offset)/params->disk->sector_size));
     }
 #endif
+    /*@ assert valid_file_recovery(file_recovery); */
     return PSTATUS_OK;
   }
+#endif
   file_recovery_new.file_stat=NULL;
   file_recovery_new.location.start=offset;
   /*@ loop invariant valid_file_recovery(file_recovery); */
@@ -205,6 +213,7 @@ inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, st
       }
     }
   }
+  /*@ assert valid_file_recovery(file_recovery); */
   return PSTATUS_OK;
 }
 #ifdef __cplusplus
diff --git a/src/poptions.h b/src/poptions.h
index 391a9e08..630d319a 100644
--- a/src/poptions.h
+++ b/src/poptions.h
@@ -30,6 +30,7 @@ extern "C" {
   @ requires \valid(current_cmd);
   @ requires valid_read_string(*current_cmd);
   @ requires \valid(options);
+  @ requires \separated(options, current_cmd, *current_cmd);
   @ ensures  valid_read_string(*current_cmd);
   @ */
 void interface_options_photorec_cli(struct ph_options *options, char**current_cmd);
diff --git a/src/refs.h b/src/refs.h
index 8a7f6ec5..f12ca4ed 100644
--- a/src/refs.h
+++ b/src/refs.h
@@ -38,6 +38,9 @@ struct ReFS_boot_sector {
   uint16_t	checksum;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ decreases 0;
+  @*/
 int check_ReFS(disk_t *disk, partition_t *partition);
 int recover_ReFS(const disk_t *disk, const struct ReFS_boot_sector *refs_header, partition_t *partition);
 
diff --git a/src/rfs.h b/src/rfs.h
index 6d47dfdb..87acb614 100644
--- a/src/rfs.h
+++ b/src/rfs.h
@@ -111,6 +111,7 @@ struct format40_super {
   @ requires \valid(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_rfs(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/savehdr.h b/src/savehdr.h
index b05504bf..94fe3f1d 100644
--- a/src/savehdr.h
+++ b/src/savehdr.h
@@ -37,17 +37,20 @@ typedef struct
 /*@
   @ requires valid_disk(disk_car);
   @ requires valid_partition(partition);
+  @ decreases 0;
   @*/
 int save_header(disk_t *disk_car, const partition_t *partition, const int verbose);
 
 /*@
   @ requires valid_disk(disk_car);
   @ requires valid_list_part(list_part);
+  @ decreases 0;
   @*/
 int partition_save(disk_t *disk_car, const list_part_t *list_part, const int verbose);
 
 /*@
   @ requires valid_disk(disk_car);
+  @ decreases 0;
   @*/
 backup_disk_t *partition_load(const disk_t *disk_car, const int verbose);
 
diff --git a/src/sessionp.h b/src/sessionp.h
index c5a1b57f..51f6127e 100644
--- a/src/sessionp.h
+++ b/src/sessionp.h
@@ -37,9 +37,11 @@ extern "C" {
 int session_load(char **cmd_device, char **current_cmd, alloc_data_t *list_free_space);
 
 /*@
-  @ requires list_free_space==\null || \valid_read(list_free_space);
-  @ requires params==\null || \valid_read(params);
-  @ requires options==\null || \valid_read(options);
+  @ requires \valid_read(list_free_space);
+  @ requires valid_ph_param(params);
+  @ requires \valid_read(options);
+  @ requires \separated(list_free_space, params, options);
+  @ ensures  valid_ph_param(params);
   @*/
 int session_save(const alloc_data_t *list_free_space, const struct ph_param *params, const struct ph_options *options);
 
diff --git a/src/sun.h b/src/sun.h
index 41784373..f0eba9b2 100644
--- a/src/sun.h
+++ b/src/sun.h
@@ -91,6 +91,7 @@ int recover_sun_i386(const disk_t *disk_car, const sun_partition_i386 *sunlabel,
   @ requires \valid(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_sun_i386(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/swap.h b/src/swap.h
index bf675666..a2b5809b 100644
--- a/src/swap.h
+++ b/src/swap.h
@@ -56,6 +56,7 @@ union swap_header {
   @ requires \valid(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_Linux_SWAP(disk_t *disk_car, partition_t *partition);
 
diff --git a/src/sysv.h b/src/sysv.h
index 7a2f175e..166dd01f 100644
--- a/src/sysv.h
+++ b/src/sysv.h
@@ -202,6 +202,9 @@ struct coh_super_block {
 	uint32_t		s_unique;	/* zero, not used */
 };
 
+/*@
+  @ decreases 0;
+  @*/
 int check_sysv(disk_t *disk_car,partition_t *partition,const int verbose);
 int recover_sysv(const disk_t *disk_car, const struct sysv4_super_block *sbd, partition_t *partition,const int verbose, const int dump_ind);
 
diff --git a/src/ufs.h b/src/ufs.h
index 5ddfb755..3c50b1f3 100644
--- a/src/ufs.h
+++ b/src/ufs.h
@@ -475,6 +475,7 @@ struct ufs_super_block {
   @ requires \valid(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_ufs(disk_t *disk_car,partition_t *partition,const int verbose);
 
diff --git a/src/vmfs.h b/src/vmfs.h
index 46024a69..9284f690 100644
--- a/src/vmfs.h
+++ b/src/vmfs.h
@@ -41,6 +41,9 @@ struct vmfs_lvm
   uint64_t blocks;
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ decreases 0;
+  @*/
 int check_VMFS(disk_t *disk,partition_t *partition);
 int recover_VMFS(const disk_t *disk, const struct vmfs_volume *sb, partition_t *partition, const int verbose, const int dump_ind);
 #ifdef __cplusplus
diff --git a/src/xfs.h b/src/xfs.h
index f55d1498..3b7b5086 100644
--- a/src/xfs.h
+++ b/src/xfs.h
@@ -38,6 +38,7 @@ extern "C" {
   @ requires \valid(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_xfs(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/zfs.h b/src/zfs.h
index 0e376305..9c5cfed0 100644
--- a/src/zfs.h
+++ b/src/zfs.h
@@ -42,6 +42,7 @@ struct vdev_boot_header {
   @ requires \valid(disk);
   @ requires \valid(partition);
   @ requires separation: \separated(disk, partition);
+  @ decreases 0;
   @*/
 int check_ZFS(disk_t *disk, partition_t *partition);