diff --git a/src/common.c b/src/common.c
index 23572aa7..6737c575 100644
--- a/src/common.c
+++ b/src/common.c
@@ -212,6 +212,7 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
   unsigned int i;
   /*@
     @ loop assigns i, partition->fsname[i];
+    @ loop invariant 0 <= i < sizeof(partition->fsname);
     @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
@@ -223,6 +224,7 @@ void set_part_name_chomp(partition_t *partition, const unsigned char *src, const
   unsigned int i;
   /*@
     @ loop assigns i, partition->fsname[i];
+    @ loop invariant 0 <= i < sizeof(partition->fsname);
     @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
@@ -375,6 +377,7 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
     unsigned int i;
     /*@
       @ loop invariant valid_read_string(src);
+      @ loop invariant 0 <= i <= n;
       @ loop assigns i, src;
       @*/
     for(i=0; i<n && src[0]!='\0'; i++)
diff --git a/src/common.h b/src/common.h
index 9a1782f3..49d3b32f 100644
--- a/src/common.h
+++ b/src/common.h
@@ -31,7 +31,6 @@ extern "C" {
 #include <string.h>
 #endif
 
-typedef struct efi_guid_s efi_guid_t;
 struct efi_guid_s
 {
   uint32_t time_low;
@@ -41,6 +40,7 @@ struct efi_guid_s
   uint8_t  clock_seq_low;
   uint8_t  node[6];
 } __attribute__ ((gcc_struct, __packed__));
+typedef struct efi_guid_s efi_guid_t;
 
 #define DEFAULT_SECTOR_SIZE     0x200u
 
diff --git a/src/crc.c b/src/crc.c
index 10dd8bd6..62bb3c80 100644
--- a/src/crc.c
+++ b/src/crc.c
@@ -91,9 +91,11 @@ unsigned int get_crc32(const void*buf, const unsigned int len, const uint32_t se
   register uint32_t crc32val;
   const unsigned char *s=(const unsigned char *)buf;
   crc32val = seed; 
-  /*@ loop assigns i, crc32val; */
+  /*@ loop invariant 0 <= i <= len;
+    @ loop assigns i, crc32val; */
   for (i = 0;  i < len;  i ++)
   {
+    /*@ assert i < len; */
     crc32val = crc32_tab[(crc32val ^ s[i]) & 0xff] ^ (crc32val >> 8);
   }
   return (unsigned int)crc32val;
diff --git a/src/file_dst.c b/src/file_dst.c
index a9bd14fa..780c0c5b 100644
--- a/src/file_dst.c
+++ b/src/file_dst.c
@@ -58,7 +58,7 @@ static int header_check_dst(const unsigned char *buffer, const unsigned int buff
   buf[7]='\0';
   if(memcmp(buffer, "LA:",3)!=0 || memcmp(&buffer[30], "\rCO:", 4)!=0)
     return 0;
-  if(sscanf(&buf, "%u", &stitch_count) < 0)
+  if(sscanf(&buf[0], "%u", &stitch_count) < 0)
     return 0;
   reset_file_recovery(file_recovery_new);
   file_recovery_new->extension=file_hint_dst.extension;
diff --git a/src/file_flv.c b/src/file_flv.c
index e74308a2..9d3713f8 100644
--- a/src/file_flv.c
+++ b/src/file_flv.c
@@ -66,6 +66,7 @@ struct flv_tag
 /*@
   @ requires file_recovery->data_check==&data_check_flv;
   @ requires valid_data_check_param(buffer, buffer_size, file_recovery);
+  @ ensures  valid_data_check_param(buffer, buffer_size, file_recovery);
   @ ensures  valid_data_check_result(\result, file_recovery);
   @ assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
   @*/
diff --git a/src/file_template.c b/src/file_template.c
index 37733700..a3b8bb73 100644
--- a/src/file_template.c
+++ b/src/file_template.c
@@ -31,7 +31,7 @@
 #include "types.h"
 #include "filegen.h"
 
-/*@ requires \valid(file_stat); */
+/*@ requires valid_register_header_check(file_stat); */
 static void register_header_check_EXTENSION(file_stat_t *file_stat);
 
 const file_hint_t file_hint_EXTENSION= {
@@ -43,6 +43,11 @@ const file_hint_t file_hint_EXTENSION= {
   .register_header_check=&register_header_check_EXTENSION
 };
 
+/*@
+  @ requires valid_file_check_param(file_recovery);
+  @ ensures  valid_file_check_result(file_recovery);
+  @ assigns  *file_recovery_new;
+  @*/
 static void file_check_EXTENSION(file_recovery_t *file_recovery)
 {
   const unsigned char EXTENSION_footer[FOOTER_SIZE]= {
@@ -51,6 +56,10 @@ static void file_check_EXTENSION(file_recovery_t *file_recovery)
   file_search_footer(file_recovery, EXTENSION_footer, sizeof(EXTENSION_footer), FOOTER_EXTRA);
 }
 
+/*@
+  @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new);
+  @ ensures  valid_header_check_result(\result, file_recovery_new);
+  @*/
 static int header_check_EXTENSION(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)
 {
   reset_file_recovery(file_recovery_new);
diff --git a/src/fnctdsk.h b/src/fnctdsk.h
index 9131a345..196aabc2 100644
--- a/src/fnctdsk.h
+++ b/src/fnctdsk.h
@@ -27,18 +27,22 @@ extern "C" {
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ assigns \nothing;
   @*/
 unsigned long int C_H_S2LBA(const disk_t *disk_car,const unsigned int C, const unsigned int H, const unsigned int S);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires \valid_read(CHS);
   @ assigns \nothing;
   @*/
-uint64_t CHS2offset(const disk_t *disk_car,const CHS_t*CHS);
+uint64_t CHS2offset(const disk_t *disk_car, const CHS_t*CHS);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.sectors_per_head > 0;
   @ assigns \nothing;
@@ -48,6 +52,7 @@ unsigned int offset2sector(const disk_t *disk_car, const uint64_t offset);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.sectors_per_head > 0;
   @ requires disk_car->geom.heads_per_cylinder > 0;
@@ -58,6 +63,7 @@ unsigned int offset2head(const disk_t *disk_car, const uint64_t offset);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.sectors_per_head > 0;
   @ requires disk_car->geom.heads_per_cylinder > 0;
@@ -67,78 +73,84 @@ unsigned int offset2cylinder(const disk_t *disk_car, const uint64_t offset);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(CHS);
   @ requires disk_car->sector_size > 0;
   @ requires disk_car->geom.sectors_per_head > 0;
   @ requires disk_car->geom.heads_per_cylinder > 0;
+  @ requires \separated(disk_car, CHS);
   @ assigns CHS->cylinder,CHS->head,CHS->sector;
   @*/
 void offset2CHS(const disk_t *disk_car,const uint64_t offset, CHS_t*CHS);
 
 /*@
-  @ requires list_disk==\null || \valid(list_disk);
-  @ requires disk==\null || (\valid(disk) && valid_read_string(disk->device));
-  @ requires the_disk==\null || \valid(the_disk);
-  @ ensures \result==\null || \valid(\result);
-  @ ensures disk==\null ==> \result == list_disk;
+  @ requires valid_list_disk(list_disk);
+  @ requires \valid(disk);
+  @ requires valid_disk(disk);
+  @ requires disk==\null || \separated(disk, \union(list_disk, the_disk));
+  @ requires the_disk==\null || (\valid_read(the_disk) && valid_disk(*the_disk) && \separated(the_disk, \union(list_disk, disk)));
+  @ decreases 0;
   @*/
+// ensures \result==\null || (\valid(\result) && valid_disk(\result->disk));
+// ensures valid_list_disk(\result);
+// ensures disk==\null ==> \result == list_disk;
+// ensures the_disk==\null || (\valid_read(the_disk) && valid_disk(*the_disk));
 list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk);
 
 /*@
-  @ requires list_disk==\null || \valid(list_disk);
-  @ requires disk_car==\null || (\valid(disk_car) && valid_read_string(disk_car->device));
-  @ ensures \result==\null || \valid(\result);
+  @ requires list_disk==\null || valid_disk(list_disk->disk);
+  @ requires \valid(disk_car);
+  @ requires valid_disk(disk_car);
+  @ requires valid_list_disk(list_disk);
+  @ requires (list_disk==\null && disk_car==\null) || \separated(list_disk, disk_car);
   @*/
+// ensures \result==\null || (\valid(\result) && valid_disk(\result->disk));
+// ensures disk_car==\null ==> \result == list_disk;
+// ensures valid_list_disk(\result);
 list_disk_t *insert_new_disk(list_disk_t *list_disk, disk_t *disk_car);
 
 /*@
   @ requires list_part == \null || \valid(list_part);
-  @ requires \valid(part);
+  @ requires valid_list_part(list_part);
+  @ requires valid_partition(part);
   @ requires \valid(insert_error);
+  @ requires (list_part==\null && part==\null) || \separated(list_part, part);
+  @ requires insert_error==\null || \valid(insert_error);
   @*/
+// ensures  valid_list_part(\result);
 list_part_t *insert_new_partition(list_part_t *list_part, partition_t *part, const int force_insert, int *insert_error);
 
 /*@
   @ requires \valid(list_part);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(\result);
   @*/
 list_part_t *sort_partition_list(list_part_t *list_part);
 
 /*@
   @ requires \valid_read(list_part);
+  @ requires valid_list_part(list_part);
+  @ ensures  valid_list_part(\result);
   @*/
 list_part_t *gen_sorted_partition_list(const list_part_t *list_part);
 
 /*@
   @ requires \valid(list_part);
+  @ requires valid_list_part(list_part);
   @*/
 void part_free_list(list_part_t *list_part);
 
 /*@
   @ requires \valid(list_part);
+  @ requires valid_list_part(list_part);
   @*/
 void part_free_list_only(list_part_t *list_part);
 
 /*@
   @ requires \valid(partition);
+  @ requires valid_partition(partition);
   @ requires \valid_read(arch);
-  @ assigns partition->part_size;
-  @ assigns partition->sborg_offset;
-  @ assigns partition->sb_offset;
-  @ assigns partition->sb_size;
-  @ assigns partition->blocksize;
-  @ assigns partition->part_type_i386;
-  @ assigns partition->part_type_sun;
-  @ assigns partition->part_type_mac;
-  @ assigns partition->part_type_xbox;
-  @ assigns partition->part_type_gpt;
-  @ assigns partition->part_uuid;
-  @ assigns partition->upart_type;
-  @ assigns partition->status;
-  @ assigns partition->order;
-  @ assigns partition->errcode;
-  @ assigns partition->fsname[0];
-  @ assigns partition->partname[0];
-  @ assigns partition->info[0];
+  @ requires \separated(partition, arch);
   @ ensures partition->part_size == 0;
   @ ensures partition->sborg_offset == 0;
   @ ensures partition->sb_offset == 0;
@@ -157,23 +169,44 @@ void part_free_list_only(list_part_t *list_part);
   @ ensures partition->info[0] == '\0';
   @ ensures partition->arch == arch;
   @*/
+  // assigns partition->part_size;
+  // assigns partition->sborg_offset;
+  // assigns partition->sb_offset;
+  // assigns partition->sb_size;
+  // assigns partition->blocksize;
+  // assigns partition->part_type_i386;
+  // assigns partition->part_type_sun;
+  // assigns partition->part_type_mac;
+  // assigns partition->part_type_xbox;
+  // assigns partition->part_type_gpt;
+  // assigns partition->part_uuid;
+  // assigns partition->upart_type;
+  // assigns partition->status;
+  // assigns partition->order;
+  // assigns partition->errcode;
+  // assigns partition->fsname[0];
+  // assigns partition->partname[0];
+  // assigns partition->info[0];
 void  partition_reset(partition_t *partition, const arch_fnct_t *arch);
 
 /*@
   @ requires \valid_read(arch);
-  @ ensures \result->arch == arch;
   @*/
+// ensures valid_partition(\result);
+// ensures \result->arch == arch;
 partition_t *partition_new(const arch_fnct_t *arch);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(list_part);
-  @ assigns \nothing;
+  @ requires valid_list_part(list_part);
   @*/
+// assigns \nothing;
 unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part_t *list_part, const int verbose);
 
 /*@
-  @ requires list_disk==\null || \valid(list_disk);
+  @ requires valid_list_disk(list_disk);
   @ requires list_disk==\null || \freeable(list_disk);
   @ requires list_disk==\null || \freeable(list_disk->disk);
   @ requires list_disk==\null || (list_disk->disk->device == \null || \freeable(list_disk->disk->device));
@@ -183,18 +216,20 @@ unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part
   @ requires list_disk==\null || (list_disk->disk->data == \null || \freeable(list_disk->disk->data));
   @ requires list_disk==\null || (list_disk->disk->rbuffer == \null || \freeable(list_disk->disk->rbuffer));
   @ requires list_disk==\null || (list_disk->disk->wbuffer == \null || \freeable(list_disk->disk->wbuffer));
+  @ decreases 0;
   @*/
 int delete_list_disk(list_disk_t *list_disk);
 
 /*@
   @ requires \valid(buffer + (0..99));
   @ ensures valid_string(buffer);
+  @ assigns buffer[0 .. 99];
   @*/
-/* TODO assigns */
 void size_to_unit(const uint64_t disk_size, char *buffer);
 
 /*@
   @ requires \valid_read(list_part);
+  @ requires valid_list_part(list_part);
   @ assigns \nothing;
   @*/
 int is_part_overlapping(const list_part_t *list_part);
@@ -202,11 +237,15 @@ int is_part_overlapping(const list_part_t *list_part);
 /*@
   @ requires \valid(dest);
   @ requires \valid_read(src);
+  @ requires \separated(src, dest);
+  @ requires valid_partition(src);
+  @ ensures  valid_partition(dest);
   @*/
 void dup_partition_t(partition_t *dest, const partition_t *src);
 
 /*@
-  @ requires list_disk==\null || \valid(list_disk);
+  @ requires valid_list_disk(list_disk);
+  @ assigns \nothing;
   @*/
 void log_disk_list(list_disk_t *list_disk);
 #ifdef __cplusplus
diff --git a/src/log.c b/src/log.c
index 64364e09..5627e15d 100644
--- a/src/log.c
+++ b/src/log.c
@@ -227,6 +227,7 @@ void dump_log(const void *nom_dump, const unsigned int lng)
   unsigned int i,j;
   unsigned int nbr_line;
   unsigned char car;
+  /*@ assert lng < UINT_MAX - 0x10; */
   nbr_line=(lng+0x10-1)/0x10;
   /* write dump to log file*/
   for (i=0; (i<nbr_line); i++)
@@ -266,6 +267,7 @@ void dump2_log(const void *dump_1, const void *dump_2, const unsigned int lng)
 {
   unsigned int i,j;
   unsigned int nbr_line;
+  /*@ requires lng < UINT_MAX - 0x08; */
   nbr_line=(lng+0x08-1)/0x08;
   /* write dump to log file*/
   for (i=0; (i<nbr_line); i++)
diff --git a/src/partgpt.h b/src/partgpt.h
index 34c93ede..115b0731 100644
--- a/src/partgpt.h
+++ b/src/partgpt.h
@@ -24,6 +24,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+#if !defined(SINGLE_PARTITION_TYPE) || defined(SINGLE_PARTITION_GPT)
 
 struct gpt_hdr
 {
@@ -63,21 +64,27 @@ struct systypes_gtp {
 };
 
 /*@
+  @ requires valid_disk(disk_car);
   @ requires \valid_read(disk_car);
-  @ requires \valid(list_part);
-  @ requires separation: \separated(disk_car, list_part, current_cmd);
+  @ requires valid_list_part(list_part);
   @ requires \valid(current_cmd);
-  @ requires valid_string(*current_cmd);
+  @ requires separation: \separated(disk_car, list_part, current_cmd, *current_cmd);
+  @ requires valid_read_string(*current_cmd);
   @*/
+// ensures  valid_list_part(\result);
+// ensures  valid_read_string(*current_cmd);
 list_part_t *add_partition_gpt_cli(const disk_t *disk_car, list_part_t *list_part, char **current_cmd);
 
 /*@
   @ requires \valid_read(disk_car);
+  @ requires valid_disk(disk_car);
   @ requires \valid(list_part);
+  @ requires valid_list_part(list_part);
   @ requires separation: \separated(disk_car, list_part);
   @*/
 int write_part_gpt(disk_t *disk_car, const list_part_t *list_part, const int ro, const int verbose);
 
+#endif
 #ifdef __cplusplus
 } /* closing brace for extern "C" */
 #endif