Lots of frama-c work that should be safe to commit

2020-06-02 17:33:50 +02:00 · 2020-06-02 17:33:50 +02:00 · b660bb8c03
commit b660bb8c03
parent 98ea5cddfe
31 changed files with 266 additions and 111 deletions
--- 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
--- 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;
 }

--- 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");
 }
--- 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 */
--- 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
--- 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
--- 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"
--- 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;
--- 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;
--- 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
--- 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);
--- 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'};
--- 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;
--- 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);
--- 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)
--- 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);
--- 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
--- 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"
--- 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;
 }
--- 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)
--- 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
--- 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
--- 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
--- 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)
--- 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>
--- 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;
--- 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)
--- 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)
  {
--- 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)
  {
--- 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;
--- 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;
 }