diff --git a/.travis.yml b/.travis.yml
index 04af5aab..3c9bd384 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -6,10 +6,8 @@ addons:
     organization: "cgsecurity-github"
     token:
       secure: "HGnOsSSghmeMHCbigtEAgkV6oaJZ1xFUhvZun0oPOv7Y2XCpIPw376G5wTppgzZUZdcSsNcu63FAnWmZZDBH29mAd6K4tIw6MDqAe9UyLzWHMEMWrMQjqSMOaqetLCw4e1Zqa0kSYyZAdg4Fp7NrNjPLho1fVUJBCCrBtU1AxaPmMNkGpSZ1d9YK6rz58jNBnm7dKp0LSUFfcas88aXKuGhGYdttdPmD4/E6XQprFGMzBMk7XXV2guKgziAprhaIAF7QOs24FhAq6IKSu00JH5UAqtgeQ9+K7srv4lHeHz/N2SzLJldrei3+WNo72T8g10enJpcerZ/lS0Tl/J+5YPsC0TAXRqZmWlbSs7CR/N6CTMlckox8tUTeDyptIYhh50xZYwR+WB4ODW5vROz7EKXVfd7YHprnMZuGMw8eJaenTZ8wm/erms38rmZNsRKqoHWXxP4QwjOJumMFJVKyq1/5MkT18lA2Ajy57WcS6SjWGyRhdirV/IGbsFdS8A21PQ0ASDA7UjJrDYclmiEfy7G1OItMv739llM2z23mN/UnKO9ijPPfi3quCSEeozQiOLQpwsdmGUhAkPfBN6dAutqIrgXl/rFV3y2KNhDprWd0GBrtNhcTLWr3/5+0rrh8ntkF904QCBvR1XwOUH4z8nmGq35WXVs4Y2aafrRw1dM="
-    branches:
-      - master
-      - dev
 
+os: linux
 language: c
 compiler:
   - gcc
diff --git a/src/common.c b/src/common.c
index 8e9e7de2..3e93f19c 100644
--- a/src/common.c
+++ b/src/common.c
@@ -24,6 +24,11 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#ifdef __FRAMAC__
+#undef HAVE_POSIX_MEMALIGN
+#undef HAVE_MEMALIGN
+#endif
  
 #include <stdio.h>
 #include <ctype.h>
@@ -51,8 +56,6 @@
 
 static int32_t secwest=0;
 
-static unsigned int up2power_aux(const unsigned int number);
-
 /* coverity[+alloc] */
 void *MALLOC(size_t size)
 {
@@ -61,7 +64,7 @@ void *MALLOC(size_t size)
   /* Warning, memory leak checker must be posix_memalign/memalign aware, otherwise  *
    * reports may look strange. Aligned memory is required if the buffer is *
    * used for read/write operation with a file opened with O_DIRECT        */
-#if defined(HAVE_POSIX_MEMALIGN) && !defined(__FRAMAC__)
+#if defined(HAVE_POSIX_MEMALIGN)
   if(size>=512)
   {
     if(posix_memalign(&res,4096,size)==0)
@@ -70,7 +73,7 @@ void *MALLOC(size_t size)
       return res;
     }
   }
-#elif defined(HAVE_MEMALIGN) && !defined(__FRAMAC__)
+#elif defined(HAVE_MEMALIGN)
   if(size>=512)
   {
     if((res=memalign(4096, size))!=NULL)
@@ -167,21 +170,16 @@ char * strcasestr (const char *haystack, const char *needle)
 }
 #endif
 
-#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__)
+#if ! defined(HAVE_LOCALTIME_R) && ! defined(__MINGW32__) && !defined(__FRAMAC__)
 struct tm *localtime_r(const time_t *timep, struct tm *result)
 {
   return localtime(timep);
 }
 #endif
 
-unsigned int up2power(const unsigned int number)
-{
-  /* log_trace("up2power(%u)=>%u\n",number, (1<<up2power_aux(number-1))); */
-  if(number==0)
-    return 1;
-  return (1<<up2power_aux(number-1));
-}
-
+/*@
+  @ assigns \nothing;
+  @*/
 static unsigned int up2power_aux(const unsigned int number)
 {
   if(number==0)
@@ -190,6 +188,13 @@ static unsigned int up2power_aux(const unsigned int number)
 	return(1+up2power_aux(number/2));
 }
 
+unsigned int up2power(const unsigned int number)
+{
+  if(number==0)
+    return 1;
+  return (1<<up2power_aux(number-1));
+}
+
 void set_part_name(partition_t *partition, const char *src, const unsigned int max_size)
 {
   unsigned int i;
@@ -275,7 +280,7 @@ time_t date_dos2unix(const unsigned short f_time, const unsigned short f_date)
 void set_secwest(void)
 {
   const time_t t = time(NULL);
-#if defined(__MINGW32__) || defined(__FRAMAC__)
+#if defined(__MINGW32__)
   const struct  tm *tmptr = localtime(&t);
 #else
   struct  tm tmp;
@@ -319,7 +324,10 @@ int check_command(char **current_cmd, const char *cmd, size_t n)
 {
   const int res=strncmp(*current_cmd, cmd, n);
   if(res==0)
+  {
     (*current_cmd)+=n;
+    return 0;
+  }
   return res;
 }
 
diff --git a/src/dfxml.c b/src/dfxml.c
index c9da693c..a101f02a 100644
--- a/src/dfxml.c
+++ b/src/dfxml.c
@@ -24,6 +24,11 @@
 #include <config.h>
 #endif
 
+#if defined(__FRAMAC__)
+#undef HAVE_LIBEWF
+#undef HAVE_SYS_UTSNAME_H
+#endif
+
 #ifdef ENABLE_DFXML
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
@@ -200,11 +205,13 @@ void xml_add_DFXML_creator(const char *package, const char *version)
 #ifdef RECORD_COMPILATION_DATE
   xml_out2s("compilation_date", get_compilation_date());
 #endif
+#ifndef MAIN_photorec
   xml_printf("<library name='libext2fs' version='%s'/>\n", td_ext2fs_version());
   xml_printf("<library name='libewf' version='%s'/>\n", td_ewf_version());
   xml_printf("<library name='libjpeg' version='%s'/>\n", td_jpeg_version());
   xml_printf("<library name='libntfs' version='%s'/>\n", td_ntfs_version());
   xml_printf("<library name='zlib' version='%s'/>\n", td_zlib_version());
+#endif
   xml_pop("build_environment");
   xml_push("execution_environment","");
 #if defined(__CYGWIN__) || defined(__MINGW32__)
@@ -238,18 +245,8 @@ void xml_add_DFXML_creator(const char *package, const char *version)
 #endif
 #ifdef HAVE_GETEUID
   xml_out2i("uid", geteuid());
-#if 0
-#ifdef HAVE_GETPWUID
-  {
-    struct passwd *tmp=getpwuid(getuid());
-    if(tmp != NULL)
-    {
-      xml_out2s("username", tmp->pw_name);
-    }
-  }
-#endif
-#endif
 #endif
+#if !defined(__FRAMAC__)
   {
     char outstr[200];
     const time_t t = time(NULL);
@@ -261,6 +258,7 @@ void xml_add_DFXML_creator(const char *package, const char *version)
       xml_out2s("start_time", outstr);
     }
   }
+#endif
   xml_pop("execution_environment");
   xml_pop("creator");
 }
diff --git a/src/dimage.c b/src/dimage.c
index d1f34835..6e651187 100644
--- a/src/dimage.c
+++ b/src/dimage.c
@@ -41,6 +41,9 @@
 #include <assert.h>
 #include <string.h>
 #include <errno.h>
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 #include "types.h"
 #include "common.h"
 #include "intrf.h"
@@ -123,6 +126,7 @@ int disk_image(disk_t *disk, const partition_t *partition, const char *image_dd)
     free(buffer);
     return -1;
   }
+#if !defined(__FRAMAC__)
   if(fstat(disk_dst, &stat_buf)==0)
   {
     int res=1;
@@ -136,6 +140,7 @@ int disk_image(disk_t *disk, const partition_t *partition, const char *image_dd)
       src_offset+=dst_offset;
     }
   }
+#endif
   src_offset_old=src_offset;
 #ifdef HAVE_NCURSES
   window=newwin(LINES, COLS, 0, 0);	/* full screen */
diff --git a/src/dir.c b/src/dir.c
index f1f0fdf9..06bd544b 100644
--- a/src/dir.c
+++ b/src/dir.c
@@ -22,6 +22,10 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#ifdef __FRAMAC__
+#undef HAVE_CHMOD
+#endif
  
 #include <stdio.h>
 #ifdef HAVE_STRING_H
diff --git a/src/ewf.h b/src/ewf.h
index 2bcf4cc1..16d2bad2 100644
--- a/src/ewf.h
+++ b/src/ewf.h
@@ -23,6 +23,10 @@
 extern "C" {
 #endif
 
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBEWF
+#endif
+
 #if defined(HAVE_LIBEWF_H) && defined(HAVE_LIBEWF)
 disk_t *fewf_init(const char *device, const int testdisk_mode);
 #endif
diff --git a/src/ext2_dir.c b/src/ext2_dir.c
index f3dc4a29..87d8a20e 100644
--- a/src/ext2_dir.c
+++ b/src/ext2_dir.c
@@ -23,6 +23,10 @@
 #include <config.h>
 #endif
 
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBEXT2FS
+#endif
+
 #include <stdio.h>
 #ifdef HAVE_STRING_H
 #include <string.h>
@@ -31,12 +35,14 @@
 #include <errno.h>
 #endif
 
+#if defined(HAVE_LIBEXT2FS)
 #ifdef HAVE_EXT2FS_EXT2_FS_H
 #include "ext2fs/ext2_fs.h"
 #endif
 #ifdef HAVE_EXT2FS_EXT2FS_H
 #include "ext2fs/ext2fs.h"
 #endif
+#endif
 
 #include "types.h"
 #include "common.h"
diff --git a/src/ext2_inc.h b/src/ext2_inc.h
index ca2421b1..e3cf9f57 100644
--- a/src/ext2_inc.h
+++ b/src/ext2_inc.h
@@ -19,6 +19,10 @@
     Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
  */
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBEXT2FS
+#endif
+
 #if defined(HAVE_LIBEXT2FS)
 struct ext2_dir_struct {
 	file_info_t *dir_list;
diff --git a/src/ext2p.c b/src/ext2p.c
index 6cbb0f7c..2e57e434 100644
--- a/src/ext2p.c
+++ b/src/ext2p.c
@@ -22,6 +22,12 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBEXT2FS
+#endif
+
+#if defined(HAVE_LIBEXT2FS)
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -48,7 +54,6 @@
 #include "log.h"
 #include "log_part.h"
 
-#ifdef HAVE_LIBEXT2FS
 unsigned int ext2_remove_used_space(disk_t *disk, const partition_t *partition, alloc_data_t *list_search_space)
 {
   dir_data_t dir_data;
diff --git a/src/fat_common.h b/src/fat_common.h
index 471c4e89..780b5cc5 100644
--- a/src/fat_common.h
+++ b/src/fat_common.h
@@ -24,10 +24,34 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+/*@
+  @ requires \valid_read(entry);
+  @ assigns \nothing;
+  @ */
 unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry);
+
+/*@
+  @ requires \valid_read(buffer + (0 .. 0x40-1));
+  @ assigns \nothing;
+  @ */
 int is_fat_directory(const unsigned char *buffer);
+
+/*@
+  @ requires \valid_read(fat_header);
+  @ assigns \nothing;
+  @ */
 unsigned int get_dir_entries(const struct fat_boot_sector *fat_header);
+
+/*@
+  @ requires \valid_read(fat_header);
+  @ assigns \nothing;
+  @ */
 unsigned int fat_sector_size(const struct fat_boot_sector *fat_header);
+
+/*@
+  @ requires \valid_read(fat_header);
+  @ assigns \nothing;
+  @ */
 unsigned int fat_sectors(const struct fat_boot_sector *fat_header);
 
 #ifdef __cplusplus
diff --git a/src/fidentify.c b/src/fidentify.c
index 090c0769..9962bc57 100644
--- a/src/fidentify.c
+++ b/src/fidentify.c
@@ -24,6 +24,11 @@
 #include <config.h>
 #endif
 
+#ifdef __FRAMAC__
+#undef HAVE_FTELLO
+#undef HAVE_DUP2
+#endif
+
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -52,6 +57,9 @@
 #include "misc.h"
 #include "file_jpg.h"
 #include "file_gz.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 
 extern file_enable_t array_file_enable[];
 extern file_check_list_t file_check_list;
@@ -119,7 +127,7 @@ static int file_identify(const char *filename, const unsigned int options)
 	off_t file_size;
 	file_recovery_new.handle=file;
 	my_fseek(file_recovery_new.handle, 0, SEEK_END);
-#if defined(HAVE_FTELLO) && !defined(__FRAMAC__)
+#if defined(HAVE_FTELLO)
 	file_size=ftello(file_recovery_new.handle);
 #else
 	file_size=ftell(file_recovery_new.handle);
@@ -258,7 +266,7 @@ int main(int argc, char **argv)
   if(log_handle!=NULL)
   {
     time_t my_time;
-#if defined(HAVE_DUP2) && !defined(__FRAMAC__)
+#if defined(HAVE_DUP2)
     dup2(fileno(log_handle),2);
 #endif
     my_time=time(NULL);
diff --git a/src/file_gz.c b/src/file_gz.c
index ba5b112d..f67cb845 100644
--- a/src/file_gz.c
+++ b/src/file_gz.c
@@ -23,6 +23,11 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#ifdef __FRAMAC__
+#undef HAVE_LIBZ
+#endif
+
 #ifdef HAVE_STRING_H
 #include <string.h>
 #endif
@@ -157,7 +162,7 @@ static int header_check_gz(const unsigned char *buffer, const unsigned int buffe
   }
   if(off >= 512 || off >= buffer_size)
     return 0;
-#if defined(HAVE_ZLIB_H) && defined(HAVE_LIBZ) && !defined(__FRAMAC__)
+#if defined(HAVE_ZLIB_H) && defined(HAVE_LIBZ)
   {
     static const unsigned char schematic_header[12]={ 0x0a, 0x00, 0x09,
       'S', 'c', 'h', 'e', 'm', 'a', 't', 'i', 'c'};
diff --git a/src/file_jpg.c b/src/file_jpg.c
index 376f1b7a..518173d6 100644
--- a/src/file_jpg.c
+++ b/src/file_jpg.c
@@ -23,6 +23,12 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#ifdef __FRAMAC__
+#undef HAVE_LIBJPEG
+#undef DEBUG_JPEG
+#endif
+
 #ifdef HAVE_STRING_H
 #include <string.h>
 #endif
@@ -661,7 +667,7 @@ static int header_check_jpg(const unsigned char *buffer, const unsigned int buff
   return 1;
 }
 
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
 struct my_error_mgr {
   struct jpeg_error_mgr pub;	/* "public" fields, must be the first field */
 
@@ -1854,7 +1860,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
     const unsigned int size=(buffer[i+2]<<8)+buffer[i+3];
     if(buffer[i]!=0xff)
     {
-#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
+#if defined(DEBUG_JPEG)
       log_info("%s no marker at 0x%x\n", file_recovery->filename, i);
 #endif
       file_recovery->offset_error=i;
@@ -1867,7 +1873,7 @@ static uint64_t jpg_check_structure(file_recovery_t *file_recovery, const unsign
       offset++;
       continue;
     }
-#if defined(DEBUG_JPEG) && !defined(__FRAMAC__)
+#if defined(DEBUG_JPEG)
     log_info("%s marker 0x%02x at 0x%x\n", file_recovery->filename, buffer[i+1], i);
 #endif
     offset+=(uint64_t)2+size;
@@ -1946,7 +1952,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
 #ifdef DEBUG_JPEG
   log_info("jpg_check_structure error at %llu\n", (long long unsigned)file_recovery->offset_error);
 #endif
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && !defined(__FRAMAC__)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
   if(thumb_offset!=0 &&
       (file_recovery->checkpoint_status==0 || thumb_error!=0) &&
       (file_recovery->offset_error==0 || thumb_offset < file_recovery->offset_error))
@@ -1974,7 +1980,7 @@ static void file_check_jpg(file_recovery_t *file_recovery)
 #endif
   if(file_recovery->offset_error!=0)
     return ;
-#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H) && ! defined(__FRAMAC__)
+#if defined(HAVE_LIBJPEG) && defined(HAVE_JPEGLIB_H)
   jpg_check_picture(file_recovery);
 #else
   file_recovery->file_size=file_recovery->calculated_file_size;
diff --git a/src/file_sig.c b/src/file_sig.c
index e75a2e84..41207e45 100644
--- a/src/file_sig.c
+++ b/src/file_sig.c
@@ -36,6 +36,9 @@
 #endif
 #include <stdio.h>
 #include <ctype.h>
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 #include "types.h"
 #include "filegen.h"
 #include "common.h"
@@ -424,12 +427,16 @@ static void register_header_check_sig(file_stat_t *file_stat)
   handle=open_signature_file();
   if(!handle)
     return;
+#ifdef __FRAMAC__
+  buffer_size=1024*1024;
+#else
   if(fstat(fileno(handle), &stat_rec)<0 || stat_rec.st_size>100*1024*1024)
   {
     fclose(handle);
     return;
   }
   buffer_size=stat_rec.st_size;
+#endif
   buffer=(char *)MALLOC(buffer_size+1);
   if(fread(buffer,1,buffer_size,handle)!=buffer_size)
   {
@@ -438,6 +445,9 @@ static void register_header_check_sig(file_stat_t *file_stat)
     return;
   }
   fclose(handle);
+#if defined(__FRAMAC__)
+  Frama_C_make_unknown(buffer, buffer_size);
+#endif
   buffer[buffer_size]='\0';
   pos=buffer;
   pos=parse_signature_file(file_stat, pos);
diff --git a/src/filegen.c b/src/filegen.c
index 70b69136..8e010f8b 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -23,6 +23,12 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#ifdef __FRAMAC__
+#undef HAVE_FTELLO
+#undef HAVE_FSEEKO
+#endif
+
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
 #endif
@@ -51,11 +57,10 @@ file_check_list_t file_check_list={
     .list = TD_LIST_HEAD_INIT(file_check_list.list)
 };
 
-static unsigned int index_header_check(void);
-
 /*@
   @ requires \valid_read(a);
   @ requires \valid_read(b);
+  @ assigns \nothing;
   @*/
 static int file_check_cmp(const struct td_list_head *a, const struct td_list_head *b)
 {
@@ -773,7 +778,7 @@ int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery
   }
 
   memcpy(&fr_test, file_recovery, sizeof(fr_test));
-#if defined(HAVE_FTELLO) && !defined(__FRAMAC__)
+#if defined(HAVE_FTELLO)
   if((offset=ftello(file_recovery->handle)) < 0)
     offset=ftell(file_recovery->handle);
 #else
@@ -858,7 +863,7 @@ void get_prev_location_smart(alloc_data_t *list_search_space, alloc_data_t **cur
 
 int my_fseek(FILE *stream, off_t offset, int whence)
 {
-#if defined(HAVE_FSEEKO) && !defined(__MINGW32__) && !defined(__ARM_EABI__) && !defined(__FRAMAC__)
+#if defined(HAVE_FSEEKO) && !defined(__MINGW32__) && !defined(__ARM_EABI__)
   {
     int res;
     if((res=fseeko(stream, offset, whence))>=0)
diff --git a/src/filegen.h b/src/filegen.h
index 2c6af8ac..dc64e4e3 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -230,9 +230,10 @@ void reset_file_recovery(file_recovery_t *file_recovery);
   @ requires \valid_function(header_check);
   @ requires \valid(file_stat);
   @*/
-void register_header_check(const unsigned int offset, const void *value, const unsigned int length, int (*header_check)(const unsigned char *buffer, const unsigned int buffer_size,
+void register_header_check(const unsigned int offset, const void *value, const unsigned int length,
+    int (*header_check)(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),
-  file_stat_t *file_stat);
+    file_stat_t *file_stat);
 
 /*@
   @ requires \valid(files_enable);
diff --git a/src/hdaccess.c b/src/hdaccess.c
index 261a0149..98be5464 100644
--- a/src/hdaccess.c
+++ b/src/hdaccess.c
@@ -22,6 +22,19 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_FSYNC
+#undef HAVE_GLOB_H
+#undef HAVE_LIBEWF
+#undef HAVE_LINUX_HDREG_H
+#undef HAVE_LINUX_TYPES_H
+#undef HAVE_PREAD
+#undef HAVE_PWRITE
+#undef HAVE_SYS_MOUNT_H
+#undef HAVE_SYS_PARAM_H
+#undef TARGET_LINUX
+#endif
  
 #ifdef HAVE_SYS_STAT_H
 #include <sys/stat.h>
@@ -38,7 +51,7 @@
 #include <stdio.h>
 #include <errno.h>
 #include "types.h"
-#ifdef HAVE_LINUX_TYPES_H
+#if defined(HAVE_LINUX_TYPES_H)
 #include <linux/types.h>
 #endif
 #include "common.h"
@@ -48,13 +61,13 @@
 #ifdef HAVE_SYS_DISKLABEL_H
 #include <sys/disklabel.h>
 #endif
-#ifdef HAVE_SYS_PARAM_H
+#if defined(HAVE_SYS_PARAM_H)
 #include <sys/param.h>
 #endif
-#ifdef HAVE_SYS_MOUNT_H
+#if defined(HAVE_SYS_MOUNT_H)
 #include <sys/mount.h>	/* BLKFLSBUF */
 #endif
-#ifdef HAVE_LINUX_HDREG_H
+#if defined(HAVE_LINUX_HDREG_H)
 #include <linux/hdreg.h>
 #endif
 #ifdef HAVE_SYS_DISK_H
@@ -104,6 +117,9 @@
 #if defined(__HAIKU__)
 #include <Drivers.h>
 #endif
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 #include "fnctdsk.h"
 #include "ewf.h"
 #include "log.h"
@@ -849,7 +865,9 @@ void update_disk_car_fields(disk_t *disk_car)
   {
     if(disk_car->geom.cylinders>0)
     {
+#ifndef __FRAMAC__
       log_warning("Fix disk size using CHS\n");
+#endif
       disk_car->disk_real_size=(uint64_t)disk_car->geom.cylinders * disk_car->geom.heads_per_cylinder *
 	disk_car->geom.sectors_per_head * disk_car->sector_size;
     }
@@ -862,8 +880,10 @@ void update_disk_car_fields(disk_t *disk_car)
       (uint64_t)disk_car->sector_size;
     if(cylinder_num>0 && disk_car->geom.cylinders != cylinder_num)
     {
+#ifndef __FRAMAC__
       log_debug("Fix cylinder count for %s: number of cylinders %lu != %lu (calculated)\n",
 	  disk_car->device, disk_car->geom.cylinders, cylinder_num);
+#endif
       disk_car->geom.cylinders = cylinder_num;
     }
   }
@@ -901,7 +921,7 @@ static char * read_device_sysfs_file (const disk_t *disk_car, const char *file)
  * information.  It uses the deprecated SCSI_IOCTL_SEND_COMMAND to
  * issue this query.
  */
-#ifdef TARGET_LINUX
+#if defined(TARGET_LINUX)
 #ifdef HAVE_SCSI_SCSI_H
 #include <scsi/scsi.h>
 #endif
diff --git a/src/hpa_dco.c b/src/hpa_dco.c
index 61d4804c..a11c5b14 100644
--- a/src/hpa_dco.c
+++ b/src/hpa_dco.c
@@ -22,7 +22,13 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
- 
+
+#if defined(__FRAMAC__)
+#undef HAVE_LINUX_TYPES_H
+#undef HAVE_LINUX_HDREG_H
+#undef HAVE_SCSI_SG_H
+#endif
+
 #ifdef HAVE_SYS_STAT_H
 #include <sys/stat.h>
 #endif
@@ -37,20 +43,20 @@
 #endif
 #include <stdio.h>
 #include "types.h"
-#ifdef HAVE_LINUX_TYPES_H
+#if defined(HAVE_LINUX_TYPES_H)
 #include <linux/types.h>
 #endif
 #include "common.h"
 #ifdef HAVE_SYS_IOCTL_H
 #include <sys/ioctl.h>
 #endif
-#ifdef HAVE_LINUX_HDREG_H
+#if defined(HAVE_LINUX_HDREG_H)
 #include <linux/hdreg.h>
 #endif
 #ifdef HAVE_FNCTL_H
 #include <fnctl.h>
 #endif
-#ifdef HAVE_SCSI_SG_H
+#if defined(HAVE_SCSI_SG_H)
 #include <scsi/sg.h>
 #endif
 #include "log.h"
diff --git a/src/intrfn.c b/src/intrfn.c
index 7c446afa..1714e2a2 100644
--- a/src/intrfn.c
+++ b/src/intrfn.c
@@ -22,9 +22,13 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
- 
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_NCURSES
+#endif
+
 #include <stdio.h>
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
 #include <stdarg.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -1173,12 +1177,9 @@ int end_ncurses(void)
   wrefresh(stdscr);
   nl();
   endwin();
-#if defined(DJGPP) || defined(__MINGW32__)
-#else
-#ifdef HAVE_DELSCREEN
+#if defined(HAVE_DELSCREEN) && !defined(DJGPP) && !defined(__MINGW32__)
   if(screenp!=NULL)
     delscreen(screenp);
-#endif
 #endif
   return 0;
 }
diff --git a/src/intrfn.h b/src/intrfn.h
index b49257e1..6c35e904 100644
--- a/src/intrfn.h
+++ b/src/intrfn.h
@@ -24,7 +24,7 @@
 extern "C" {
 #endif
 
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES) && !defined(MAIN_photorec)
 #ifdef HAVE_NCURSES_H
 #include <ncurses.h>
 #elif defined(HAVE_NCURSESW_NCURSES_H)
diff --git a/src/misc.c b/src/misc.c
index fb89ce81..c887e018 100644
--- a/src/misc.c
+++ b/src/misc.c
@@ -24,6 +24,12 @@
 #include <config.h>
 #endif
 
+#if defined(__FRAMAC__)
+#undef HAVE_STRPTIME
+#undef HAVE_SYS_UTSNAME_H
+#undef HAVE_UNAME
+#endif
+
 #include <string.h>
 #include <ctype.h>
 #include <stdarg.h>
@@ -172,7 +178,7 @@ https://msdn.microsoft.com/en-us/library/windows/desktop/ms724834%28v=vs.85%29.a
   }
 #elif defined(DJGPP)
   return "DOS";
-#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME) && !defined(__FRAMAC__)
+#elif defined(HAVE_SYS_UTSNAME_H) && defined(HAVE_UNAME)
   {
     struct utsname Ver;
     if(uname(&Ver)==0)
@@ -281,7 +287,7 @@ const char *get_compilation_date(void)
 {
   static char buffer[100] = {0x00};
 #ifdef __DATE__ 
-#if defined(HAVE_STRPTIME) && !defined(__FRAMAC__)
+#if defined(HAVE_STRPTIME)
   struct tm tm;
   memset(&tm,0,sizeof(tm));
   if(strptime(__DATE__, "%b %d %Y", &tm)!=NULL)
@@ -299,6 +305,7 @@ const char *get_compilation_date(void)
 #endif
 #endif
 #endif
+  /*@ assert valid_read_string(&buffer[0]); */
   return buffer;
 }
 #endif
diff --git a/src/ntfs_dir.c b/src/ntfs_dir.c
index 878aa335..a544f35b 100644
--- a/src/ntfs_dir.c
+++ b/src/ntfs_dir.c
@@ -26,6 +26,12 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBNTFS
+#undef HAVE_LIBNTFS3G
+#undef HAVE_SYS_PARAM_H
+#endif
  
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -43,7 +49,7 @@
 #ifdef HAVE_ERRNO_H
 #include <errno.h>
 #endif
-#ifdef HAVE_SYS_PARAM_H
+#if defined(HAVE_SYS_PARAM_H)
 #include <sys/param.h>
 #endif
 #ifdef HAVE_MACHINE_ENDIAN_H
@@ -56,14 +62,14 @@
 #include <stdarg.h>
 #include "types.h"
 
-#ifdef HAVE_LIBNTFS
+#if defined(HAVE_LIBNTFS)
 #include <ntfs/volume.h>
 #include <ntfs/attrib.h>
 #ifdef HAVE_NTFS_VERSION_H
 #include <ntfs/version.h>
 #endif
 #endif
-#ifdef HAVE_LIBNTFS3G
+#if defined(HAVE_LIBNTFS3G)
 #include <ntfs-3g/volume.h>
 #include <ntfs-3g/attrib.h>
 #endif
diff --git a/src/ntfs_io.c b/src/ntfs_io.c
index 7f57edd0..5ca494a5 100644
--- a/src/ntfs_io.c
+++ b/src/ntfs_io.c
@@ -25,8 +25,13 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBNTFS
+#undef HAVE_LIBNTFS3G
+#endif
  
-#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
+#if (defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G))
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
 #endif
diff --git a/src/ntfsp.c b/src/ntfsp.c
index b6a040ae..86330c7e 100644
--- a/src/ntfsp.c
+++ b/src/ntfsp.c
@@ -23,6 +23,13 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_LIBNTFS
+#undef HAVE_LIBNTFS3G
+#endif
+
+#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -44,9 +51,7 @@
 #ifdef HAVE_LIBNTFS3G
 #include <ntfs-3g/attrib.h>
 #endif
-#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
 #include "ntfsp.h"
-#endif
 #include "intrf.h"
 #include "dir.h"
 #include "ntfs.h"
@@ -55,7 +60,6 @@
 #include "log.h"
 #include "log_part.h"
 
-#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G)
 #define SIZEOF_BUFFER ((const unsigned int)512)
 
 unsigned int ntfs_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space)
diff --git a/src/partxboxn.c b/src/partxboxn.c
index a504bd17..83468e24 100644
--- a/src/partxboxn.c
+++ b/src/partxboxn.c
@@ -25,7 +25,11 @@
 #include <config.h>
 #endif
 
-#ifdef HAVE_NCURSES
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_NCURSES
+#endif
+
+#if defined(HAVE_NCURSES)
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
diff --git a/src/pdiskseln.c b/src/pdiskseln.c
index b7ed7b50..b119d068 100644
--- a/src/pdiskseln.c
+++ b/src/pdiskseln.c
@@ -28,6 +28,10 @@
 #undef SUDO_BIN
 #endif
 
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_NCURSES
+#endif
+
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -41,7 +45,7 @@
 #include "types.h"
 #include "common.h"
 #include "intrf.h"
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
 #include "intrfn.h"
 #endif
 #include "dir.h"
@@ -60,7 +64,7 @@
 #include "chgarch.h"
 #include "chgarchn.h"
 
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
 #define NBR_DISK_MAX 		(LINES-6-8)
 #define INTER_DISK_X		0
 #define INTER_DISK_Y		(8+NBR_DISK_MAX)
@@ -70,7 +74,7 @@
 extern const arch_fnct_t arch_none;
 
 
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
 static int photorec_disk_selection_ncurses(struct ph_param *params, struct ph_options *options, const list_disk_t *list_disk, alloc_data_t *list_search_space)
 {
   int command;
@@ -273,12 +277,12 @@ int do_curses_photorec(struct ph_param *params, struct ph_options *options, cons
     char *saved_cmd=NULL;
     session_load(&saved_device, &saved_cmd,&list_search_space);
     if(saved_device!=NULL && saved_cmd!=NULL && !td_list_empty(&list_search_space.list)
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
 	&& ( resume_session!=0 || ask_confirmation("Continue previous session ? (Y/N)")!=0)
 #endif
       )
     {
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
       {
 	WINDOW *window=newwin(LINES, COLS, 0, 0);	/* full screen */
 	aff_copy(window);
@@ -305,7 +309,7 @@ int do_curses_photorec(struct ph_param *params, struct ph_options *options, cons
   if(params->cmd_device!=NULL && params->cmd_run!=NULL)
   {
     params->disk=photorec_disk_selection_cli(params->cmd_device, list_disk, &list_search_space);
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
     if(params->disk==NULL)
     {
       log_critical("No disk found\n");
@@ -328,7 +332,7 @@ int do_curses_photorec(struct ph_param *params, struct ph_options *options, cons
     return 0;
 #endif
   }
-#ifdef HAVE_NCURSES
+#if defined(HAVE_NCURSES)
   return photorec_disk_selection_ncurses(params, options, list_disk, &list_search_space);
 #else
   return 0;
diff --git a/src/phcfg.c b/src/phcfg.c
index ef5a2668..f5f4853c 100644
--- a/src/phcfg.c
+++ b/src/phcfg.c
@@ -81,23 +81,11 @@ static FILE *file_options_save_aux(void)
     }
   }
 #endif
-#ifndef DJGPP
+#if !defined(DJGPP) && !defined(__FRAMAC__)
   if(filename==NULL)
   {
     char *home;
     home = getenv("HOME");
-#if 0
-    /* Using 'getpwuid' in statically linked applications requires at
-       runtime the shared libraries from the glibc version used for linking
-    */
-    if (home == NULL) 
-    {
-      struct passwd *pw;
-      pw = getpwuid(getuid());
-      if (pw != NULL)
-	home = pw->pw_dir;
-    }
-#endif
     if (home != NULL)
     {
       filename=(char*)MALLOC(strlen(home)+strlen(DOT_PHOTOREC_CFG)+1);
@@ -157,22 +145,10 @@ static FILE *file_options_load_aux(void)
     }
   }
 #endif
-#ifndef DJGPP
+#if !defined(DJGPP) && !defined(__FRAMAC__)
   {
     char *home;
     home = getenv("HOME");
-#if 0
-    /* Using 'getpwuid' in statically linked applications requires at
-       runtime the shared libraries from the glibc version used for linking
-    */
-    if (home == NULL) 
-    {
-      struct passwd *pw;
-      pw = getpwuid(getuid());
-      if (pw != NULL)
-	home = pw->pw_dir;
-    }
-#endif
     if (home != NULL)
     {
       FILE*handle;
@@ -232,6 +208,9 @@ int file_options_load(file_enable_t *files_enable)
   {
     const char *extension=&buffer[0];
     char *extension_status;
+#ifdef __FRAMAC__
+  Frama_C_make_unknown(buffer, sizeof(buffer)-1);
+#endif
     buffer[sizeof(buffer)-1]='\0';
     extension_status=strchr(buffer,',');
     if(extension_status!=NULL)
diff --git a/src/phmain.c b/src/phmain.c
index 5f9864fc..943b153f 100644
--- a/src/phmain.c
+++ b/src/phmain.c
@@ -28,6 +28,11 @@
 #undef SUDO_BIN
 #endif
 
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_DUP2
+#undef HAVE_LIBEWF
+#endif
+
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -335,7 +340,7 @@ int main( int argc, char **argv )
   if(log_handle!=NULL)
   {
     time_t my_time;
-#ifdef HAVE_DUP2
+#if defined(HAVE_DUP2)
     dup2(fileno(log_handle),2);
 #endif
     my_time=time(NULL);
@@ -351,8 +356,10 @@ int main( int argc, char **argv )
 #ifdef RECORD_COMPILATION_DATE
   log_info("Compilation date: %s\n", get_compilation_date());
 #endif
+#ifndef MAIN_photorec
   log_info("ext2fs lib: %s, ntfs lib: %s, ewf lib: %s, libjpeg: %s, curses lib: %s\n",
       td_ext2fs_version(), td_ntfs_version(), td_ewf_version(), td_jpeg_version(), td_curses_version());
+#endif
 #if defined(HAVE_GETEUID) && !defined(__CYGWIN__) && !defined(__MINGW32__) && !defined(DJGPP)
   if(geteuid()!=0)
   {
diff --git a/src/photorec.c b/src/photorec.c
index c84d54c9..bc0cb95b 100644
--- a/src/photorec.c
+++ b/src/photorec.c
@@ -24,6 +24,13 @@
 #include <config.h>
 #endif
 
+#if defined(__FRAMAC__) || defined(MAIN_photorec)
+#undef HAVE_FTRUNCATE
+#undef HAVE_LIBEXT2FS
+#undef HAVE_LIBNTFS
+#undef HAVE_LIBNTFS3G
+#endif
+
 #include <stdio.h>
 #ifdef HAVE_STDLIB_H
 #include <stdlib.h>
@@ -41,6 +48,9 @@
 #ifdef HAVE_SYS_TIME_H
 #include <sys/time.h>
 #endif
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 #include "types.h"
 #include "common.h"
 #include "fnctdsk.h"
@@ -88,7 +98,7 @@ void del_search_space(alloc_data_t *list_search_space, const uint64_t start, con
 /*@
   @ requires \valid(list_search_space);
   @ requires new_current_search_space == \null || \valid(*new_current_search_space);
-  @ requires offset == \null || \valid(*offset);
+  @ 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)
 {
@@ -339,7 +349,7 @@ unsigned int remove_used_space(disk_t *disk_car, const partition_t *partition, a
   else if(partition->upart_type==UP_NTFS)
     return ntfs_remove_used_space(disk_car, partition, list_search_space);
 #endif
-#ifdef HAVE_LIBEXT2FS
+#if defined(HAVE_LIBEXT2FS)
   else if(partition->upart_type==UP_EXT2 || partition->upart_type==UP_EXT3 || partition->upart_type==UP_EXT4)
     return ext2_remove_used_space(disk_car, partition, list_search_space);
 #endif
@@ -558,7 +568,7 @@ static void file_finish_aux(file_recovery_t *file_recovery, struct ph_param *par
     unlink(file_recovery->filename);
     return;
   }
-#ifdef HAVE_FTRUNCATE
+#if defined(HAVE_FTRUNCATE)
   fflush(file_recovery->handle);
   if(ftruncate(fileno(file_recovery->handle), file_recovery->file_size)<0)
   {
diff --git a/src/sessionp.c b/src/sessionp.c
index 7d8c39de..e5510316 100644
--- a/src/sessionp.c
+++ b/src/sessionp.c
@@ -42,6 +42,9 @@
 #include <stdlib.h>
 #endif
 #include <errno.h>
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
 #include "types.h"
 #include "common.h"
 #include "intrf.h"
@@ -70,12 +73,17 @@ int session_load(char **cmd_device, char **current_cmd, alloc_data_t *list_free_
     session_save(NULL, NULL, NULL);
     return -1;
   }
-  if(fstat(fileno(f_session), &stat_rec)<0)
-    buffer_size=SESSION_MAXSIZE;
-  else
+#ifndef __FRAMAC__
+  if(fstat(fileno(f_session), &stat_rec)>=0)
     buffer_size=stat_rec.st_size;
+  else
+#endif
+    buffer_size=SESSION_MAXSIZE;
   buffer=(char *)MALLOC(buffer_size+1);
   taille=fread(buffer,1,buffer_size,f_session);
+#if defined(__FRAMAC__)
+  Frama_C_make_unknown(buffer, buffer_size);
+#endif
   buffer[taille]='\0';
   fclose(f_session);
   pos=buffer;
diff --git a/src/setdate.c b/src/setdate.c
index 5e26e1ac..23fd1082 100644
--- a/src/setdate.c
+++ b/src/setdate.c
@@ -22,6 +22,11 @@
 #ifdef HAVE_CONFIG_H
 #include <config.h>
 #endif
+
+#if defined(__FRAMAC__)
+#undef HAVE_UTIME
+#endif
+
 #include "types.h"
 #ifdef HAVE_UTIME_H
 #include <utime.h>
@@ -49,12 +54,10 @@ int set_date(const char *pathname, time_t actime, time_t modtime)
     return -1;
   ut.actime  = actime;
   ut.modtime = modtime;
-#ifndef __FRAMAC__
   if (utime(pathname, &ut)) {
     log_error("ERROR: Couldn't set the file's date and time for %s\n", pathname);
     return -1;
   }
-#endif
 #endif
   return 0;
 }