1 files changed, 81 insertions, 22 deletions

diff --git a/src/fnctdsk.c b/src/fnctdsk.c
index b6a7487f..ea0dcd49 100644
--- a/src/fnctdsk.c
+++ b/src/fnctdsk.c
@@ -59,6 +59,7 @@ uint64_t CHS2offset(const disk_t *disk_car,const CHS_t*CHS)
 {
   return (((uint64_t)CHS->cylinder * disk_car->geom.heads_per_cylinder + CHS->head) *
       disk_car->geom.sectors_per_head + CHS->sector - 1) * disk_car->sector_size;
+//  return (uint64_t)C_H_S2LBA(disk_car, CHS->cylinder, CHS->head, CHS->sector) * disk_car->sector_size;
 }
 
 unsigned int offset2sector(const disk_t *disk_car, const uint64_t offset)
@@ -111,40 +112,72 @@ void dup_partition_t(partition_t *dst, const partition_t *src)
 #endif
 }
 
+/*@
+  @ requires valid_list_disk(list_disk);
+  @ requires disk!=\null;
+  @ requires valid_disk(disk);
+  @ assigns \nothing;
+  @*/
+static disk_t *search_disk(const list_disk_t *list_disk, const disk_t *disk)
+{
+  const list_disk_t *tmp;
+  /*@
+    @ loop assigns tmp;
+    @*/
+  for(tmp=list_disk;tmp!=NULL;tmp=tmp->next)
+  {
+    if(tmp->disk->device!=NULL && disk->device!=NULL &&
+	strcmp(tmp->disk->device, disk->device)==0)
+    {
+      return tmp->disk;
+    }
+  }
+  return NULL;
+}
+
 list_disk_t *insert_new_disk_aux(list_disk_t *list_disk, disk_t *disk, disk_t **the_disk)
 {
-  list_disk_t *tmp;
   list_disk_t *prev=NULL;
   list_disk_t *new_disk;
+  disk_t *found;
   if(disk==NULL)
   {
     if(the_disk!=NULL)
       *the_disk=NULL;
+    /*@ assert valid_list_disk(list_disk); */
     return list_disk;
   }
-  /* Add it at the end if it doesn't already exist */
-  for(tmp=list_disk;tmp!=NULL;tmp=tmp->next)
+  found=search_disk(list_disk, disk);
+  /* Do not add a disk already known */
+  if(found!=NULL)
   {
-    if(tmp->disk->device!=NULL && disk->device!=NULL &&
-	strcmp(tmp->disk->device, disk->device)==0)
-    {
-      disk->clean(disk);
-      if(the_disk!=NULL)
-	*the_disk=tmp->disk;
-      return list_disk;
-    }
-    prev=tmp;
+    disk->clean(disk);
+    if(the_disk!=NULL)
+      *the_disk=found;
+    /*@ assert valid_list_disk(list_disk); */
+    return list_disk;
+  }
+  /* Add the disk at the end */
+  {
+    list_disk_t *tmp;
+    /*@
+      @ loop assigns tmp,prev;
+      @*/
+    for(tmp=list_disk;tmp!=NULL;tmp=tmp->next)
+      prev=tmp;
   }
   new_disk=(list_disk_t *)MALLOC(sizeof(*new_disk));
   new_disk->disk=disk;
+  new_disk->prev=prev;
+  new_disk->next=NULL;
   if(prev!=NULL)
   {
     prev->next=new_disk;
   }
-  new_disk->prev=prev;
-  new_disk->next=NULL;
   if(the_disk!=NULL)
     *the_disk=disk;
+  /*@ assert valid_list_disk(new_disk); */
+  /*@ assert valid_list_disk(list_disk); */
   return (list_disk!=NULL?list_disk:new_disk);
 }
 
@@ -222,6 +255,10 @@ list_part_t *sort_partition_list(list_part_t *list_part)
   list_part_t *new_list_part=NULL;
   list_part_t *element;
   list_part_t *next;
+  /*@ assert valid_list_part(new_list_part); */
+  /*@
+    @ loop invariant valid_list_part(new_list_part);
+    @*/
   for(element=list_part;element!=NULL;element=next)
   {
     int insert_error=0;
@@ -231,6 +268,7 @@ list_part_t *sort_partition_list(list_part_t *list_part)
       free(element->part);
     free(element);
   }
+  /*@ assert valid_list_part(new_list_part); */
   return new_list_part;
 }
 
@@ -238,12 +276,17 @@ list_part_t *gen_sorted_partition_list(const list_part_t *list_part)
 {
   list_part_t *new_list_part=NULL;
   const list_part_t *element;
+  /*@ assert valid_list_part(new_list_part); */
+  /*@
+    @ loop invariant valid_list_part(new_list_part);
+    @*/
   for(element=list_part;element!=NULL;element=element->next)
   {
     int insert_error=0;
     if(element->part->status!=STATUS_DELETED)
       new_list_part=insert_new_partition(new_list_part, element->part, 1, &insert_error);
   }
+  /*@ assert valid_list_part(new_list_part); */
   return new_list_part;
 }
 
@@ -252,6 +295,7 @@ void part_free_list(list_part_t *list_part)
 {
   list_part_t *element;
   element=list_part;
+  /*@ loop invariant valid_list_part(element); */
   while(element!=NULL)
   {
     list_part_t *next=element->next;
@@ -266,6 +310,7 @@ void part_free_list_only(list_part_t *list_part)
 {
   list_part_t *element;
   element=list_part;
+  /*@ loop invariant valid_list_part(element); */
   while(element!=NULL)
   {
     list_part_t *next=element->next;
@@ -283,6 +328,9 @@ int is_part_overlapping(const list_part_t *list_part)
   if(list_part==NULL)
     return 0;
   element=list_part;
+  /*@
+    @ loop assigns element;
+    @*/
   while(1)
   {
     const list_part_t *next=element->next;
@@ -313,7 +361,9 @@ void  partition_reset(partition_t *partition, const arch_fnct_t *arch)
   partition->part_type_mac=PMAC_UNK;
   partition->part_type_xbox=PXBOX_UNK;
   partition->part_type_gpt=GPT_ENT_TYPE_UNUSED;
+#ifndef DISABLED_FOR_FRAMAC
   guid_cpy(&partition->part_uuid, &GPT_ENT_TYPE_UNUSED);
+#endif
   partition->upart_type=UP_UNK;
   partition->status=STATUS_DELETED;
   partition->order=NO_ORDER;
@@ -357,7 +407,7 @@ static unsigned int get_geometry_from_list_part_aux(const disk_t *disk_car, cons
       }
     }
   }
-#ifndef __FRAMAC__
+#ifndef DISABLED_FOR_FRAMAC
   if(nbr>0)
   {
     log_info("get_geometry_from_list_part_aux head=%u nbr=%u\n",
@@ -387,26 +437,29 @@ unsigned int get_geometry_from_list_part(const disk_t *disk_car, const list_part
   unsigned int best_score;
   unsigned int i;
   unsigned int heads_per_cylinder=disk_car->geom.heads_per_cylinder;
-  disk_t *new_disk_car=(disk_t *)MALLOC(sizeof(*new_disk_car));
-  memcpy(new_disk_car,disk_car,sizeof(*new_disk_car));
-  best_score=get_geometry_from_list_part_aux(new_disk_car, list_part, verbose);
+  disk_t new_disk_car;
+  memcpy(&new_disk_car,disk_car,sizeof(new_disk_car));
+  best_score=get_geometry_from_list_part_aux(&new_disk_car, list_part, verbose);
+  /*@ loop assigns i, best_score, heads_per_cylinder, new_disk_car.geom.heads_per_cylinder; */
   for(i=0; head_list[i]!=0; i++)
   {
     unsigned int score;
-    new_disk_car->geom.heads_per_cylinder=head_list[i];
-    score=get_geometry_from_list_part_aux(new_disk_car, list_part, verbose);
+    new_disk_car.geom.heads_per_cylinder=head_list[i];
+    score=get_geometry_from_list_part_aux(&new_disk_car, list_part, verbose);
     if(score >= best_score)
     {
       best_score=score;
-      heads_per_cylinder=new_disk_car->geom.heads_per_cylinder;
+      heads_per_cylinder=new_disk_car.geom.heads_per_cylinder;
     }
   }
-  free(new_disk_car);
   return heads_per_cylinder;
 }
 
 void size_to_unit(const uint64_t disk_size, char *buffer)
 {
+#ifdef DISABLED_FOR_FRAMAC
+  buffer[0]='\0';
+#else
   if(disk_size<(uint64_t)10*1024)
     sprintf(buffer,"%u B", (unsigned)disk_size);
   else if(disk_size<(uint64_t)10*1024*1024)
@@ -417,13 +470,18 @@ void size_to_unit(const uint64_t disk_size, char *buffer)
     sprintf(buffer,"%u GB / %u GiB", (unsigned)(disk_size/1000/1000/1000), (unsigned)(disk_size/1024/1024/1024));
   else
     sprintf(buffer,"%u TB / %u TiB", (unsigned)(disk_size/1000/1000/1000/1000), (unsigned)(disk_size/1024/1024/1024/1024));
+#endif
 }
 
 void log_disk_list(list_disk_t *list_disk)
 {
+#ifndef DISABLED_FOR_FRAMAC
   list_disk_t *element_disk;
   /* save disk parameters to rapport */
   log_info("Hard disk list\n");
+  /*@
+    @ loop invariant valid_list_disk(list_disk);
+    @*/
   for(element_disk=list_disk;element_disk!=NULL;element_disk=element_disk->next)
   {
     disk_t *disk=element_disk->disk;
@@ -437,4 +495,5 @@ void log_disk_list(list_disk_t *list_disk)
     log_info("\n");
   }
   log_info("\n");
+#endif
 }