From b660bb8c035f1dbc5e01007e14917faa6b7a9d82 Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Tue, 2 Jun 2020 17:33:50 +0200 Subject: [PATCH] Lots of frama-c work that should be safe to commit --- .travis.yml | 4 +--- src/common.c | 36 ++++++++++++++++++++++-------------- src/dfxml.c | 20 +++++++++----------- src/dimage.c | 5 +++++ src/dir.c | 4 ++++ src/ewf.h | 4 ++++ src/ext2_dir.c | 6 ++++++ src/ext2_inc.h | 4 ++++ src/ext2p.c | 7 ++++++- src/fat_common.h | 24 ++++++++++++++++++++++++ src/fidentify.c | 12 ++++++++++-- src/file_gz.c | 7 ++++++- src/file_jpg.c | 16 +++++++++++----- src/file_sig.c | 10 ++++++++++ src/filegen.c | 13 +++++++++---- src/filegen.h | 5 +++-- src/hdaccess.c | 30 +++++++++++++++++++++++++----- src/hpa_dco.c | 14 ++++++++++---- src/intrfn.c | 13 +++++++------ src/intrfn.h | 2 +- src/misc.c | 11 +++++++++-- src/ntfs_dir.c | 12 +++++++++--- src/ntfs_io.c | 7 ++++++- src/ntfsp.c | 10 +++++++--- src/partxboxn.c | 6 +++++- src/pdiskseln.c | 18 +++++++++++------- src/phcfg.c | 31 +++++-------------------------- src/phmain.c | 9 ++++++++- src/photorec.c | 16 +++++++++++++--- src/sessionp.c | 14 +++++++++++--- src/setdate.c | 7 +++++-- 31 files changed, 266 insertions(+), 111 deletions(-) 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 #endif + +#ifdef __FRAMAC__ +#undef HAVE_POSIX_MEMALIGN +#undef HAVE_MEMALIGN +#endif #include #include @@ -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< #endif +#if defined(__FRAMAC__) +#undef HAVE_LIBEWF +#undef HAVE_SYS_UTSNAME_H +#endif + #ifdef ENABLE_DFXML #include #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("\n", td_ext2fs_version()); xml_printf("\n", td_ewf_version()); xml_printf("\n", td_jpeg_version()); xml_printf("\n", td_ntfs_version()); xml_printf("\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 #include #include +#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 #endif + +#ifdef __FRAMAC__ +#undef HAVE_CHMOD +#endif #include #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 #endif +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_LIBEXT2FS +#endif + #include #ifdef HAVE_STRING_H #include @@ -31,12 +35,14 @@ #include #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 #endif + +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_LIBEXT2FS +#endif + +#if defined(HAVE_LIBEXT2FS) #include #ifdef HAVE_STDLIB_H #include @@ -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 #endif +#ifdef __FRAMAC__ +#undef HAVE_FTELLO +#undef HAVE_DUP2 +#endif + #include #ifdef HAVE_STDLIB_H #include @@ -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 #endif + +#ifdef __FRAMAC__ +#undef HAVE_LIBZ +#endif + #ifdef HAVE_STRING_H #include #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 #endif + +#ifdef __FRAMAC__ +#undef HAVE_LIBJPEG +#undef DEBUG_JPEG +#endif + #ifdef HAVE_STRING_H #include #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 #include +#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 #endif + +#ifdef __FRAMAC__ +#undef HAVE_FTELLO +#undef HAVE_FSEEKO +#endif + #ifdef HAVE_STDLIB_H #include #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 #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 @@ -38,7 +51,7 @@ #include #include #include "types.h" -#ifdef HAVE_LINUX_TYPES_H +#if defined(HAVE_LINUX_TYPES_H) #include #endif #include "common.h" @@ -48,13 +61,13 @@ #ifdef HAVE_SYS_DISKLABEL_H #include #endif -#ifdef HAVE_SYS_PARAM_H +#if defined(HAVE_SYS_PARAM_H) #include #endif -#ifdef HAVE_SYS_MOUNT_H +#if defined(HAVE_SYS_MOUNT_H) #include /* BLKFLSBUF */ #endif -#ifdef HAVE_LINUX_HDREG_H +#if defined(HAVE_LINUX_HDREG_H) #include #endif #ifdef HAVE_SYS_DISK_H @@ -104,6 +117,9 @@ #if defined(__HAIKU__) #include #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 #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 #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 #endif @@ -37,20 +43,20 @@ #endif #include #include "types.h" -#ifdef HAVE_LINUX_TYPES_H +#if defined(HAVE_LINUX_TYPES_H) #include #endif #include "common.h" #ifdef HAVE_SYS_IOCTL_H #include #endif -#ifdef HAVE_LINUX_HDREG_H +#if defined(HAVE_LINUX_HDREG_H) #include #endif #ifdef HAVE_FNCTL_H #include #endif -#ifdef HAVE_SCSI_SG_H +#if defined(HAVE_SCSI_SG_H) #include #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 #endif - + +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_NCURSES +#endif + #include -#ifdef HAVE_NCURSES +#if defined(HAVE_NCURSES) #include #ifdef HAVE_STDLIB_H #include @@ -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 #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 #endif +#if defined(__FRAMAC__) +#undef HAVE_STRPTIME +#undef HAVE_SYS_UTSNAME_H +#undef HAVE_UNAME +#endif + #include #include #include @@ -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 #endif + +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_LIBNTFS +#undef HAVE_LIBNTFS3G +#undef HAVE_SYS_PARAM_H +#endif #ifdef HAVE_STDLIB_H #include @@ -43,7 +49,7 @@ #ifdef HAVE_ERRNO_H #include #endif -#ifdef HAVE_SYS_PARAM_H +#if defined(HAVE_SYS_PARAM_H) #include #endif #ifdef HAVE_MACHINE_ENDIAN_H @@ -56,14 +62,14 @@ #include #include "types.h" -#ifdef HAVE_LIBNTFS +#if defined(HAVE_LIBNTFS) #include #include #ifdef HAVE_NTFS_VERSION_H #include #endif #endif -#ifdef HAVE_LIBNTFS3G +#if defined(HAVE_LIBNTFS3G) #include #include #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 #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 #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 #endif + +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_LIBNTFS +#undef HAVE_LIBNTFS3G +#endif + +#if defined(HAVE_LIBNTFS) || defined(HAVE_LIBNTFS3G) #include #ifdef HAVE_STDLIB_H #include @@ -44,9 +51,7 @@ #ifdef HAVE_LIBNTFS3G #include #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 #endif -#ifdef HAVE_NCURSES +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_NCURSES +#endif + +#if defined(HAVE_NCURSES) #include #ifdef HAVE_STDLIB_H #include 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 #ifdef HAVE_STDLIB_H #include @@ -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 #ifdef HAVE_STDLIB_H #include @@ -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 #endif +#if defined(__FRAMAC__) || defined(MAIN_photorec) +#undef HAVE_FTRUNCATE +#undef HAVE_LIBEXT2FS +#undef HAVE_LIBNTFS +#undef HAVE_LIBNTFS3G +#endif + #include #ifdef HAVE_STDLIB_H #include @@ -41,6 +48,9 @@ #ifdef HAVE_SYS_TIME_H #include #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 #endif #include +#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 #endif + +#if defined(__FRAMAC__) +#undef HAVE_UTIME +#endif + #include "types.h" #ifdef HAVE_UTIME_H #include @@ -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; }