summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-08-07 08:23:46 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-08-07 08:23:46 +0200
commit28d21ab0894b850206aaaa4c83e28355851c6e04 (patch)
tree0136878f750fe0bea26ba0dca8f08653ebbec9b4
parent5106d055ca96376f5dc678908cac74e2774bf0cf (diff)
move code from photorec_new_file() to photorec_header_found() that was
the only caller. It should be easier to understand.
-rw-r--r--src/photorec_check_header.h53
1 files changed, 32 insertions, 21 deletions
diff --git a/src/photorec_check_header.h b/src/photorec_check_header.h
index ed41ff7..a6797ce 100644
--- a/src/photorec_check_header.h
+++ b/src/photorec_check_header.h
@@ -72,26 +72,22 @@ static void photorec_dir_fat(const unsigned char *buffer, const unsigned int rea
}
}
-static pstatus_t photorec_new_file(file_recovery_t *file_recovery, struct ph_param *params, const uint64_t offset)
-{
- set_filename(file_recovery, params);
- if(file_recovery->file_stat->file_hint->recover==1)
- {
-#if defined(__CYGWIN__) || defined(__MINGW32__)
- file_recovery->handle=fopen_with_retry(file_recovery->filename,"w+b");
-#else
- file_recovery->handle=fopen(file_recovery->filename,"w+b");
-#endif
- if(!file_recovery->handle)
- {
- log_critical("Cannot create file %s: %s\n", file_recovery->filename, strerror(errno));
- params->offset=offset;
- return PSTATUS_EACCES;
- }
- }
- return PSTATUS_OK;
-}
-
+/*@
+ @ requires \valid_read(file_recovery_new);
+ @ requires \valid(file_recovery);
+ @ requires file_recovery->extension == \null || valid_read_string(file_recovery->extension);
+ @ requires \valid(file_recovery->file_stat);
+ @ requires \valid(file_recovery->file_stat->file_hint);
+ @ requires valid_read_string(file_recovery->file_stat->file_hint->description);
+ @ requires \valid(params);
+ @ requires \valid(params->disk);
+ @ requires \valid_read(options);
+ @ requires \valid(list_search_space);
+ @ requires \valid(buffer + (0 .. params->blocksize -1));
+ @ requires params->disk->sector_size > 0;
+ @ ensures \result == PSTATUS_OK || \result == PSTATUS_EACCES;
+ @ ensures *file_recovered == PFSTATUS_BAD || *file_recovered == PFSTATUS_OK || *file_recovered == PFSTATUS_OK_TRUNCATED;
+ @*/
static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new, file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset)
{
*file_recovered=PFSTATUS_BAD;
@@ -121,7 +117,22 @@ static pstatus_t photorec_header_found(const file_recovery_t *file_recovery_new,
const unsigned int read_size=(blocksize>65536?blocksize:65536);
photorec_dir_fat(buffer, read_size, file_recovery->location.start/params->disk->sector_size);
}
- return photorec_new_file(file_recovery, params, offset);
+ set_filename(file_recovery, params);
+ if(file_recovery->file_stat->file_hint->recover==1)
+ {
+#if defined(__CYGWIN__) || defined(__MINGW32__)
+ file_recovery->handle=fopen_with_retry(file_recovery->filename,"w+b");
+#else
+ file_recovery->handle=fopen(file_recovery->filename,"w+b");
+#endif
+ if(!file_recovery->handle)
+ {
+ log_critical("Cannot create file %s: %s\n", file_recovery->filename, strerror(errno));
+ params->offset=offset;
+ return PSTATUS_EACCES;
+ }
+ }
+ return PSTATUS_OK;
}
inline static pstatus_t photorec_check_header(file_recovery_t *file_recovery, struct ph_param *params, const struct ph_options *options, alloc_data_t *list_search_space, const unsigned char *buffer, pfstatus_t *file_recovered, const uint64_t offset)