diff --git a/src/lvm.h b/src/lvm.h
index f2bebbf2..f48a62fe 100644
--- a/src/lvm.h
+++ b/src/lvm.h
@@ -95,6 +95,7 @@ typedef struct {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_LVM(disk_t *disk_car, partition_t *partition, const int verbose);
 
@@ -129,7 +130,9 @@ struct lvm2_pv_header {
   uint64_t device_size_xl;        /* Bytes */
   /* NULL-terminated list of data areas followed by */
   /* NULL-terminated list of metadata area headers */
+#if !defined(__FRAMAC__)
   struct lvm2_disk_locn disk_areas_xl[0];      /* Two lists */
+#endif
 } __attribute__ ((packed));
 
 /*@
@@ -137,6 +140,7 @@ struct lvm2_pv_header {
   @ requires valid_disk(disk_car);
   @ requires \valid(partition);
   @ requires separation: \separated(disk_car, partition);
+  @ decreases 0;
   @*/
 int check_LVM2(disk_t *disk_car, partition_t *partition, const int verbose);
 
diff --git a/src/md.c b/src/md.c
index 993fb200..f042070e 100644
--- a/src/md.c
+++ b/src/md.c
@@ -36,10 +36,12 @@
 #include "fnctdsk.h"
 #include "log.h"
 
+#ifndef __FRAMAC__
 static int test_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, const partition_t *partition, const int dump_ind)
 {
   if(le32(sb->md_magic)!=(unsigned int)MD_SB_MAGIC)
     return 1;
+#ifndef __FRAMAC__
   log_info("\nRaid magic value at %u/%u/%u\n",
       offset2cylinder(disk_car,partition->part_offset),
       offset2head(disk_car,partition->part_offset),
@@ -50,6 +52,7 @@ static int test_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, co
     /* chunk_size may be 0 */
     log_info("Raid chunk size: %llu bytes\n", (long long unsigned)le32(sb->chunk_size));
   }
+#endif
   if(le32(sb->major_version)>1)
     return 1;
   if(dump_ind!=0)
@@ -64,6 +67,7 @@ static int test_MD_be(const disk_t *disk_car, const struct mdp_superblock_s *sb,
 {
   if(be32(sb->md_magic)!=(unsigned int)MD_SB_MAGIC)
     return 1;
+#ifndef __FRAMAC__
   log_info("\nRaid magic value at %u/%u/%u\n",
       offset2cylinder(disk_car,partition->part_offset),
       offset2head(disk_car,partition->part_offset),
@@ -74,6 +78,7 @@ static int test_MD_be(const disk_t *disk_car, const struct mdp_superblock_s *sb,
     /* chunk_size may be 0 */
     log_info("Raid chunk size: %llu bytes\n",(long long unsigned)be32(sb->chunk_size));
   }
+#endif
   if(be32(sb->major_version)>1)
     return 1;
   if(dump_ind!=0)
@@ -122,6 +127,7 @@ static void set_MD_info(const struct mdp_superblock_s *sb, partition_t *partitio
 	(unsigned int)le32(sb1->major_version),
 	(unsigned int)le32(sb1->level),
 	(long unsigned)le32(sb1->dev_number));
+#ifndef __FRAMAC__
     if(le32(sb1->max_dev) <= 384)
     {
       unsigned int i,d;
@@ -143,9 +149,12 @@ static void set_MD_info(const struct mdp_superblock_s *sb, partition_t *partitio
       }
       strcat(partition->info, ")");
     }
+#endif
   }
+#ifndef __FRAMAC__
   if(verbose>0)
     log_info("%s %s\n", partition->fsname, partition->info);
+#endif
 }
 
 static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *partition, const int verbose)
@@ -186,6 +195,7 @@ static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *parti
 	(unsigned int)be32(sb1->major_version),
 	(unsigned int)be32(sb1->level),
 	(long unsigned)be32(sb1->dev_number));
+#if !defined(__FRAMAC__)
     if(be32(sb1->max_dev) <= 384)
     {
       unsigned int i,d;
@@ -207,13 +217,18 @@ static void set_MD_info_be(const struct mdp_superblock_s *sb, partition_t *parti
       }
       strcat(partition->info, ")");
     }
+#endif
   }
+#ifndef __FRAMAC__
   if(verbose>0)
     log_info("%s %s\n", partition->fsname, partition->info);
+#endif
 }
+#endif
 
 int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
 {
+#ifndef __FRAMAC__
   unsigned char *buffer=(unsigned char*)MALLOC(MD_SB_BYTES);
   /* MD version 1.1 */
   if(disk_car->pread(disk_car, buffer, MD_SB_BYTES, partition->part_offset) == MD_SB_BYTES)
@@ -224,7 +239,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
 	le64(sb1->super_offset)==0 &&
 	test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
     {
+#ifndef __FRAMAC__
       log_info("check_MD 1.1\n");
+#endif
       set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
       free(buffer);
       return 0;
@@ -234,7 +251,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
 	 be64(sb1->super_offset)==0 &&
         test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
     {
+#ifndef __FRAMAC__
       log_info("check_MD 1.1 (BigEndian)\n");
+#endif
       set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
       free(buffer);
       return 0;
@@ -249,7 +268,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
         le64(sb1->super_offset)==8 &&
         test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
     {
+#ifndef __FRAMAC__
       log_info("check_MD 1.2\n");
+#endif
       set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
       free(buffer);
       return 0;
@@ -259,7 +280,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
         be64(sb1->super_offset)==8 &&
         test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
     {
+#ifndef __FRAMAC__
       log_info("check_MD 1.2 (BigEndian)\n");
+#endif
       set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
       free(buffer);
       return 0;
@@ -269,17 +292,21 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
   {
     const struct mdp_superblock_s *sb=(const struct mdp_superblock_s *)buffer;
     const uint64_t offset=MD_NEW_SIZE_SECTORS(partition->part_size/512)*512;
+#ifndef __FRAMAC__
     if(verbose>1)
     {
       log_verbose("Raid md 0.90 offset %llu\n", (long long unsigned)offset/512);
     }
+#endif
     if(disk_car->pread(disk_car, buffer, MD_SB_BYTES, partition->part_offset + offset) == MD_SB_BYTES)
     {
       if(le32(sb->md_magic)==(unsigned int)MD_SB_MAGIC &&
 	  le32(sb->major_version)==0 &&
 	  test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
       {
+#ifndef __FRAMAC__
         log_info("check_MD 0.90\n");
+#endif
         set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
         free(buffer);
         return 0;
@@ -288,7 +315,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
 	  be32(sb->major_version)==0 &&
 	  test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
       {
+#ifndef __FRAMAC__
         log_info("check_MD 0.90 (BigEndian)\n");
+#endif
         set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
         free(buffer);
         return 0;
@@ -299,10 +328,12 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
   if(partition->part_size > 8*2*512)
   {
     const uint64_t offset=(uint64_t)(((partition->part_size/512)-8*2) & ~(4*2-1))*512;
+#ifndef __FRAMAC__
     if(verbose>1)
     {
       log_verbose("Raid md 1.0 offset %llu\n", (long long unsigned)offset/512);
     }
+#endif
     if(disk_car->pread(disk_car, buffer, MD_SB_BYTES, partition->part_offset + offset) == MD_SB_BYTES)
     {
       const struct mdp_superblock_1 *sb1=(const struct mdp_superblock_1 *)buffer;
@@ -311,7 +342,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
           le64(sb1->super_offset)==(offset/512) &&
           test_MD(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
       {
+#ifndef __FRAMAC__
         log_info("check_MD 1.0\n");
+#endif
         set_MD_info((struct mdp_superblock_s*)buffer, partition, verbose);
         free(buffer);
         return 0;
@@ -321,7 +354,9 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
           be64(sb1->super_offset)==(offset/512) &&
           test_MD_be(disk_car, (struct mdp_superblock_s*)buffer, partition, 0)==0)
       {
+#ifndef __FRAMAC__
         log_info("check_MD 1.0 (BigEndian)\n");
+#endif
         set_MD_info_be((struct mdp_superblock_s*)buffer, partition, verbose);
         free(buffer);
         return 0;
@@ -329,11 +364,13 @@ int check_MD(disk_t *disk_car, partition_t *partition, const int verbose)
     }
   }
   free(buffer);
+#endif
   return 1;
 }
 
 int recover_MD_from_partition(disk_t *disk_car, partition_t *partition, const int verbose)
 {
+#ifndef __FRAMAC__
   unsigned char *buffer=(unsigned char*)MALLOC(MD_SB_BYTES);
   /* MD version 0.90 */
   {
@@ -365,11 +402,13 @@ int recover_MD_from_partition(disk_t *disk_car, partition_t *partition, const in
   }
   /* md 1.1 & 1.2 don't need special operation to be recovered */
   free(buffer);
+#endif
   return 1;
 }
 
 int recover_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, partition_t *partition, const int verbose, const int dump_ind)
 {
+#ifndef __FRAMAC__
   if(test_MD(disk_car, sb, partition, dump_ind)==0)
   {
     set_MD_info(sb, partition, verbose);
@@ -410,5 +449,6 @@ int recover_MD(const disk_t *disk_car, const struct mdp_superblock_s *sb, partit
     }
     return 0;
   }
+#endif
   return 1;
 }
diff --git a/src/md.h b/src/md.h
index eb579f48..76da2da1 100644
--- a/src/md.h
+++ b/src/md.h
@@ -242,7 +242,9 @@ struct mdp_superblock_1 {
 	 * into the 'roles' value.  If a device is spare or faulty, then it doesn't
 	 * have a meaningful role.
 	 */
+#if !defined(__FRAMAC__)
 	uint16_t	dev_roles[0];	/* role in array, or 0xffff for a spare, or 0xfffe for faulty */
+#endif
 };
 
 #if 0
diff --git a/src/ntfs_struct.h b/src/ntfs_struct.h
index 7c3b25ec..98b70672 100644
--- a/src/ntfs_struct.h
+++ b/src/ntfs_struct.h
@@ -199,7 +199,9 @@ typedef struct {
 /* 40*/	uint8_t file_name_length;			/* Length of file name in
 						   (Unicode) characters. */
 /* 41*/	uint8_t file_name_type;	/* Namespace of the file name.*/
+#if !defined(__FRAMAC__)
 /* 42*/	char *file_name[0];			/* File name in Unicode. */
+#endif
 } __attribute__((gcc_struct, __packed__)) TD_FILE_NAME_ATTR;
 
 
diff --git a/src/wbfs.h b/src/wbfs.h
index 1f784e19..b1d30ef6 100644
--- a/src/wbfs.h
+++ b/src/wbfs.h
@@ -35,9 +35,14 @@ struct wbfs_head
   uint8_t  hd_sec_sz_s;       	// sector size in this partition
   uint8_t  wbfs_sec_sz_s;     	// size of a wbfs sec
   uint8_t  padding3[2];
+#if !defined(__FRAMAC__)
   uint8_t  disc_table[0];    	// size depends on hd sector size
+#endif
 } __attribute__ ((gcc_struct, __packed__));
 
+/*@
+  @ decreases 0;
+  @*/
 int check_WBFS(disk_t *disk,partition_t *partition);
 int recover_WBFS(const disk_t *disk, const struct wbfs_head *sb, partition_t *partition, const int verbose, const int dump_ind);
 #ifdef __cplusplus