summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/file_ace.c8
-rw-r--r--src/file_amd.c4
-rw-r--r--src/file_amr.c3
-rw-r--r--src/file_arj.c8
-rw-r--r--src/file_bmp.c4
-rw-r--r--src/file_dir.c2
-rw-r--r--src/file_fits.c4
-rw-r--r--src/file_found.h5
-rw-r--r--src/file_gz.c1
-rw-r--r--src/file_list.c2
-rw-r--r--src/file_mlv.c1
-rw-r--r--src/file_png.c1
-rw-r--r--src/file_template.c1
-rw-r--r--src/file_tiff.c4
-rw-r--r--src/file_tivo.c26
-rw-r--r--src/filegen.c2
-rw-r--r--src/filegen.h3
17 files changed, 42 insertions, 37 deletions
diff --git a/src/file_ace.c b/src/file_ace.c
index a39e170..3d63685 100644
--- a/src/file_ace.c
+++ b/src/file_ace.c
@@ -111,10 +111,8 @@ static int check_ace_crc(FILE *handle, const unsigned int len, const unsigned in
}
/*@
- @ requires \valid(file_recovery);
+ @ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery->handle);
- @ requires \valid_read(&file_recovery->extension);
- @ requires valid_read_string(file_recovery->extension);
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ requires \initialized(&file_recovery->time);
@
@@ -143,9 +141,7 @@ static void file_check_ace(file_recovery_t *file_recovery)
{
return ;
}
-#ifdef __FRAMAC__
- Frama_C_make_unknown(&buffer, sizeof(buffer));
-#endif
+ /*@ assert \initialized(&buffer + (0 .. sizeof(buffer)-1)); */
#ifdef DEBUG_ACE
log_info("file_ace: Block header at 0x%08lx: CRC16=0x%04X size=%u type=%u"
" flags=0x%04X addsize=%u\n",
diff --git a/src/file_amd.c b/src/file_amd.c
index d7ed82a..eb05fdb 100644
--- a/src/file_amd.c
+++ b/src/file_amd.c
@@ -51,9 +51,9 @@ const file_hint_t file_hint_amd= {
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
- @ assigns *file_recovery_new;
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
+ @ assigns *file_recovery_new;
@*/
static int header_check_amd(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)
{
@@ -73,9 +73,9 @@ static int header_check_amd(const unsigned char *buffer, const unsigned int buff
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_amd, buffer+(..), file_recovery, file_recovery_new);
- @ assigns *file_recovery_new;
@ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
+ @ assigns *file_recovery_new;
@*/
static int header_check_amt(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)
{
diff --git a/src/file_amr.c b/src/file_amr.c
index 9b76d25..2e91205 100644
--- a/src/file_amr.c
+++ b/src/file_amr.c
@@ -94,8 +94,9 @@ static data_check_t data_check_amr(const unsigned char *buffer, const unsigned i
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_amr, buffer+(..), file_recovery, file_recovery_new);
- @ assigns *file_recovery_new;
+ @ ensures \result == 0 || \result == 1;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
+ @ assigns *file_recovery_new;
@*/
static int header_check_amr(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)
{
diff --git a/src/file_arj.c b/src/file_arj.c
index c86a795..e2e392d 100644
--- a/src/file_arj.c
+++ b/src/file_arj.c
@@ -119,13 +119,13 @@ struct arj_main_header {
} __attribute__ ((gcc_struct, __packed__));
/*@
+ @ requires \valid(file_recovery);
@ requires valid_file_recovery(file_recovery);
@ requires \separated(file_recovery, file_recovery->handle, file_recovery->extension, &errno, &Frama_C_entropy_source);
@ requires file_recovery->file_check == &file_check_arj;
+ @ ensures \valid(file_recovery->handle);
@ assigns *file_recovery->handle, errno, file_recovery->file_size;
@ assigns Frama_C_entropy_source;
- @
- @ ensures \valid(file_recovery->handle);
@*/
static void file_check_arj(file_recovery_t *file_recovery)
{
@@ -134,14 +134,14 @@ static void file_check_arj(file_recovery_t *file_recovery)
}
/*@
- @ requires buffer_size > sizeof(struct arj_main_header);
+ @ requires buffer_size >= sizeof(struct arj_main_header);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ requires valid_file_recovery(file_recovery);
@ requires \valid(file_recovery_new);
@ requires file_recovery_new->blocksize > 0;
@ requires separation: \separated(&file_hint_arj, buffer+(..), file_recovery, file_recovery_new);
- @ assigns *file_recovery_new;
@ ensures \result!=0 ==> valid_file_recovery(file_recovery_new);
+ @ assigns *file_recovery_new;
@*/
static int header_check_arj(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)
{
diff --git a/src/file_bmp.c b/src/file_bmp.c
index b2d56b0..841ed92 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -99,10 +99,8 @@ struct bmp_header
@ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
@ ensures (\result == 1) ==> (file_recovery_new->file_rename == \null);
@ ensures (\result == 1) ==> (valid_read_string(file_recovery_new->extension));
- @ ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
- @ ensures *buffer==\old(*buffer);
@*/
- /* TODO ensures *file_recovery==\old(*file_recovery); */
+// ensures (\result == 1) ==> \separated(file_recovery_new, file_recovery_new->extension);
static int header_check_bmp(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)
{
const struct bmp_header *bm=(const struct bmp_header *)buffer;
diff --git a/src/file_dir.c b/src/file_dir.c
index 1abbf0f..54a9777 100644
--- a/src/file_dir.c
+++ b/src/file_dir.c
@@ -66,6 +66,7 @@ static void file_rename_fatdir(file_recovery_t *file_recovery)
fclose(file);
if(buffer_size<32)
return;
+ /*@ assert buffer_size >= 32; */
cluster=fat_get_cluster_from_entry((const struct msdos_dir_entry *)&buffer[0]);
sprintf(buffer_cluster, "cluster_%u", cluster);
file_rename(file_recovery, buffer_cluster, strlen(buffer_cluster), 0, NULL, 1);
@@ -109,6 +110,7 @@ static int header_check_dir(const unsigned char *buffer, const unsigned int buff
file_recovery_new->file_check=&file_check_size;
file_recovery_new->file_rename=&file_rename_fatdir;
file_recovery_new->time=date_dos2unix(le16(de->time),le16(de->date));
+ /*@ assert valid_file_recovery(file_recovery_new); */
return 1;
}
diff --git a/src/file_fits.c b/src/file_fits.c
index 5882573..ff2ba0c 100644
--- a/src/file_fits.c
+++ b/src/file_fits.c
@@ -118,7 +118,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
if(tmp > PHOTOREC_MAX_FILE_SIZE)
naxis_size=0;
else if(tmp>0)
- {
+ { /* FIXME overflow */
naxis_size*=(tmp+8-1)/8;
}
}
@@ -135,7 +135,7 @@ static uint64_t fits_info(const unsigned char *buffer, const unsigned int buffer
if(naxis_val > PHOTOREC_MAX_FILE_SIZE)
naxis_size=0;
else
- {
+ { /* FIXME overflow */
naxis_size*=naxis_val;
}
}
diff --git a/src/file_found.h b/src/file_found.h
index e03f319..9607c40 100644
--- a/src/file_found.h
+++ b/src/file_found.h
@@ -25,6 +25,11 @@
extern "C" {
#endif
+/*@
+ @ requires \valid(current_search_space);
+ @ requires \valid(file_stat);
+ @ requires \separated(current_search_space, file_stat);
+ @*/
alloc_data_t *file_found(alloc_data_t *current_search_space, const uint64_t offset, file_stat_t *file_stat);
#ifdef __cplusplus
diff --git a/src/file_gz.c b/src/file_gz.c
index 3cb6282..33b017a 100644
--- a/src/file_gz.c
+++ b/src/file_gz.c
@@ -249,6 +249,7 @@ static int header_check_gz(const unsigned char *buffer, const unsigned int buffe
#endif
if(file_recovery->file_check==&file_check_bgzf)
{
+ /*@ assert \valid_function(file_recovery->file_check); */
header_ignored(file_recovery_new);
return 0;
}
diff --git a/src/file_list.c b/src/file_list.c
index 962d9ab..0ab9e9f 100644
--- a/src/file_list.c
+++ b/src/file_list.c
@@ -371,7 +371,7 @@ extern const file_hint_t file_hint_zpr;
file_enable_t array_file_enable[]=
{
-#if (!defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_sig)) && !defined(__FRAMAC__)
+#if ((!defined(SINGLE_FORMAT) && !defined(__FRAMAC__)) || defined(SINGLE_FORMAT_sig))
{ .enable=0, .file_hint=&file_hint_sig },
#endif
#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_1cd)
diff --git a/src/file_mlv.c b/src/file_mlv.c
index 00fc6cd..2f2d9db 100644
--- a/src/file_mlv.c
+++ b/src/file_mlv.c
@@ -161,6 +161,7 @@ static void file_check_mlv(file_recovery_t *file_recovery)
/*@
@ requires valid_file_recovery(file_recovery);
+ @ requires file_recovery->file_rename == &file_rename_mlv;
@*/
static void file_rename_mlv(file_recovery_t *file_recovery)
{
diff --git a/src/file_png.c b/src/file_png.c
index 00be0be..1f66ec8 100644
--- a/src/file_png.c
+++ b/src/file_png.c
@@ -41,6 +41,7 @@
extern const file_hint_t file_hint_doc;
+/*@ requires \valid(file_stat); */
static void register_header_check_png(file_stat_t *file_stat);
static data_check_t data_check_png(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
static data_check_t data_check_mng(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery);
diff --git a/src/file_template.c b/src/file_template.c
index eb1f052..3773370 100644
--- a/src/file_template.c
+++ b/src/file_template.c
@@ -31,6 +31,7 @@
#include "types.h"
#include "filegen.h"
+/*@ requires \valid(file_stat); */
static void register_header_check_EXTENSION(file_stat_t *file_stat);
const file_hint_t file_hint_EXTENSION= {
diff --git a/src/file_tiff.c b/src/file_tiff.c
index cf79e73..17edb1f 100644
--- a/src/file_tiff.c
+++ b/src/file_tiff.c
@@ -20,7 +20,7 @@
*/
-#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT) || defined(SINGLE_FORMAT_tiff) || defined(SINGLE_FORMAT_jpg) || defined(SINGLE_FORMAT_rw2) || defined(SINGLE_FORMAT_orf) || defined(SINGLE_FORMAT_wdp)
#ifdef HAVE_CONFIG_H
#include <config.h>
#endif
@@ -185,7 +185,7 @@ static void register_header_check_tiff(file_stat_t *file_stat)
{
static const unsigned char tiff_header_be[4]= { 'M','M',0x00, 0x2a};
static const unsigned char tiff_header_le[4]= { 'I','I',0x2a, 0x00};
-#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf)
+#if !defined(SINGLE_FORMAT_jpg) && !defined(SINGLE_FORMAT_rw2) && !defined(SINGLE_FORMAT_orf) && !defined(SINGLE_FORMAT_wdp)
#if !defined(MAIN_tiff_le) && !defined(MAIN_jpg)
register_header_check(0, tiff_header_be, sizeof(tiff_header_be), &header_check_tiff_be, file_stat);
#endif
diff --git a/src/file_tivo.c b/src/file_tivo.c
index 966f257..a739e67 100644
--- a/src/file_tivo.c
+++ b/src/file_tivo.c
@@ -34,13 +34,13 @@
/*@ requires \valid(file_stat); */
static void register_header_check_tivo(file_stat_t *file_stat);
-const file_hint_t file_hint_tivo= {
- .extension="TiVo",
- .description="TiVo video record",
- .max_filesize=PHOTOREC_MAX_FILE_SIZE,
- .recover=1,
- .enable_by_default=1,
- .register_header_check=&register_header_check_tivo
+const file_hint_t file_hint_tivo = {
+ .extension = "TiVo",
+ .description = "TiVo video record",
+ .max_filesize = PHOTOREC_MAX_FILE_SIZE,
+ .recover = 1,
+ .enable_by_default = 1,
+ .register_header_check = &register_header_check_tivo
};
/*@
@@ -54,7 +54,7 @@ const file_hint_t file_hint_tivo= {
@*/
static void file_check_tivo(file_recovery_t *file_recovery)
{
- const unsigned char tivo_footer[8]= {
+ const unsigned char tivo_footer[8] = {
0x00, 0x00, 0x01, 0xb7, 0x00, 0x00, 0x01, 0xb9
};
file_search_footer(file_recovery, tivo_footer, sizeof(tivo_footer), 0);
@@ -73,18 +73,18 @@ static void file_check_tivo(file_recovery_t *file_recovery)
@*/
static int header_check_tivo(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)
{
- if(memcmp(&buffer[0x1c], "<?xml ", 6)!=0)
+ if(memcmp(&buffer[0x1c], "<?xml ", 6) != 0)
return 0;
reset_file_recovery(file_recovery_new);
- file_recovery_new->extension=file_hint_tivo.extension;
- file_recovery_new->file_check=&file_check_tivo;
+ file_recovery_new->extension = file_hint_tivo.extension;
+ file_recovery_new->file_check = &file_check_tivo;
return 1;
}
static void register_header_check_tivo(file_stat_t *file_stat)
{
- static const unsigned char tivo_header[7]= {
- 'T' , 'i' , 'V' , 'o' , 0x00, 0x04, 0x00
+ static const unsigned char tivo_header[7] = {
+ 'T', 'i', 'V', 'o', 0x00, 0x04, 0x00
};
register_header_check(0, tivo_header, sizeof(tivo_header), &header_check_tivo, file_stat);
}
diff --git a/src/filegen.c b/src/filegen.c
index f1b457a..d8bdbff 100644
--- a/src/filegen.c
+++ b/src/filegen.c
@@ -758,7 +758,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end)
/* 0: file_recovery_new->location.start has been taken into account, offset_skipped_header may have been updated
* 1: file_recovery_new->location.start has been ignored */
/*@
- @ requires separation: \separated(file_recovery, file_recovery_new, &errno, &offset_skipped_header);
+ @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno, &offset_skipped_header);
@*/
int header_ignored_adv(const file_recovery_t *file_recovery, const file_recovery_t *file_recovery_new)
{
diff --git a/src/filegen.h b/src/filegen.h
index 415d906..1c94ab0 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -319,7 +319,7 @@ void header_ignored_cond_reset(uint64_t start, uint64_t end);
void header_ignored(const file_recovery_t *file_recovery_new);
/*@
- @ requires separation: \separated(file_recovery, file_recovery_new, &errno);
+ @ requires separation: \separated(file_recovery, file_recovery->handle, file_recovery_new, &errno);
@ requires \valid_read(file_recovery);
@ requires \valid_read(file_recovery_new);
@ requires valid_file_recovery(file_recovery);
@@ -327,7 +327,6 @@ void header_ignored(const file_recovery_t *file_recovery_new);
@ requires \valid_function(file_recovery->file_check);
@ requires \initialized(&file_recovery->file_check);
@ requires \initialized(&file_recovery->handle);
- @ requires \separated(file_recovery, file_recovery->handle);
@ ensures \result == 0 || \result == 1;
@*/
// ensures valid_file_recovery(file_recovery);
generated by cgit v1.1 at 2021-04-11 05:09:06 +0000