summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-09-21 10:13:53 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-09-21 10:13:53 +0200
commit0f09fa0121746225324e1a5ed70f5705bc1b6042 (patch)
tree8f2199a46552949ade16641559ee553f4c00164a
parent5e48555814c93598b109eccf8cdf2b2b69621c88 (diff)
PhotoRec: add frama-c tests for bmp
-rw-r--r--src/file_bmp.c135
1 files changed, 127 insertions, 8 deletions
diff --git a/src/file_bmp.c b/src/file_bmp.c
index f20326a..dfc824b 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -30,9 +30,11 @@
#include "types.h"
#include "filegen.h"
#include "common.h"
+#if defined(__FRAMAC__)
+#include "__fc_builtin.h"
+#endif
static void register_header_check_bmp(file_stat_t *file_stat);
-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 file_hint_t file_hint_bmp= {
.extension="bmp",
@@ -45,28 +47,43 @@ const file_hint_t file_hint_bmp= {
static const unsigned char bmp_header[2]= {'B','M'};
-static void register_header_check_bmp(file_stat_t *file_stat)
-{
- register_header_check(0, bmp_header,sizeof(bmp_header), &header_check_bmp, file_stat);
-}
-
struct bmp_header
{
uint16_t magic;
uint32_t size;
uint32_t reserved;
uint32_t offset;
+ uint32_t hdr_size;
} __attribute__ ((gcc_struct, __packed__));
+/*@
+ @ requires buffer_size >= 18;
+ @ requires \valid_read(buffer+(0..buffer_size-1));
+ @ requires \valid_read(file_recovery);
+ @ requires \valid(file_recovery_new);
+ @ requires file_recovery_new->blocksize > 0;
+ @ ensures \result == 0 || \result == 1;
+ @ ensures (\result == 1) ==> (file_recovery_new->extension == file_hint_bmp.extension);
+ @ ensures (\result == 1) ==> (file_recovery_new->calculated_file_size >= 65);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_size == 0);
+ @ ensures (\result == 1) ==> (file_recovery_new->min_filesize == 65);
+ @ ensures (\result == 1) ==> (file_recovery_new->data_check == &data_check_size);
+ @ ensures (\result == 1) ==> (file_recovery_new->file_check == &file_check_size);
+ @*/
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;
- if(buffer[0]=='B' && buffer[1]=='M' && bm->reserved==0 &&
+ if(buffer[0]!='B' || buffer[1]!='M')
+ return 0;
+ if(bm->reserved!=0)
+ return 0;
+ if(
(buffer[14]==12 || buffer[14]==64 || buffer[14]==40 || buffer[14]==52 ||
buffer[14]==56 || buffer[14]==108 || buffer[14]==124) &&
buffer[15]==0 && buffer[16]==0 && buffer[17]==0 &&
le32(bm->offset) < le32(bm->size) &&
- le32(bm->size) >= 65)
+ le32(bm->size) >= 65 &&
+ le32(bm->hdr_size) < le32(bm->size))
{
/* See http://en.wikipedia.org/wiki/BMP_file_format */
reset_file_recovery(file_recovery_new);
@@ -75,7 +92,109 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
file_recovery_new->calculated_file_size=(uint64_t)le32(bm->size);
file_recovery_new->data_check=&data_check_size;
file_recovery_new->file_check=&file_check_size;
+ /*@ assert file_recovery_new->extension == file_hint_bmp.extension; */
+ /*@ assert file_recovery_new->calculated_file_size >= 65; */
+ /*@ assert file_recovery_new->file_size == 0; */
+ /*@ assert file_recovery_new->min_filesize == 65; */
+ /*@ assert file_recovery_new->data_check == &data_check_size; */
+ /*@ assert file_recovery_new->file_check == &file_check_size; */
return 1;
}
return 0;
}
+
+static void register_header_check_bmp(file_stat_t *file_stat)
+{
+ register_header_check(0, bmp_header,sizeof(bmp_header), &header_check_bmp, file_stat);
+}
+
+#if defined(MAIN_bmp)
+#define BLOCKSIZE 65536u
+int main()
+{
+ unsigned char buffer[BLOCKSIZE];
+ int res;
+ file_recovery_t file_recovery_new;
+ file_recovery_t file_recovery;
+ file_stat_t file_stats;
+
+ /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+
+ reset_file_recovery(&file_recovery);
+ file_recovery.blocksize=BLOCKSIZE;
+ file_recovery_new.blocksize=BLOCKSIZE;
+ file_recovery_new.data_check=NULL;
+ file_recovery_new.file_stat=NULL;
+ file_recovery_new.file_check=NULL;
+ file_recovery_new.file_rename=NULL;
+ file_recovery_new.calculated_file_size=0;
+ file_recovery_new.file_size=0;
+ file_recovery_new.location.start=0;
+
+ file_stats.file_hint=&file_hint_bmp;
+ file_stats.not_recovered=0;
+ file_stats.recovered=0;
+ file_hint_bmp.register_header_check(&file_stats);
+ if(header_check_bmp(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
+ return 0;
+ memcpy(file_recovery_new.filename, "demo", 5);
+ /*@ assert file_recovery_new.extension == file_hint_bmp.extension; */
+ /*@ assert file_recovery_new.calculated_file_size >= 65; */
+ /*@ assert file_recovery_new.file_size == 0; */
+ /*@ assert file_recovery_new.min_filesize == 65; */
+ /*@ assert file_recovery_new.file_check == &file_check_size; */
+ /*@ assert file_recovery_new.data_check == &data_check_size; */
+ file_recovery_new.file_stat=&file_stats;
+ /*@ assert file_recovery_new.file_stat->file_hint!=NULL; */
+ if(file_recovery_new.data_check!=NULL)
+ {
+ unsigned char big_buffer[2*BLOCKSIZE];
+ data_check_t res_data_check=DC_CONTINUE;
+ memset(big_buffer, 0, BLOCKSIZE);
+ memcpy(big_buffer + BLOCKSIZE, buffer, BLOCKSIZE);
+ /*@ assert file_recovery_new.data_check == &data_check_size; */
+ /*@ assert file_recovery_new.file_size == 0; */;
+ /*@ assert file_recovery_new.file_size <= file_recovery_new.calculated_file_size; */;
+ res_data_check=file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ file_recovery_new.file_size+=BLOCKSIZE;
+ if(res_data_check == DC_CONTINUE)
+ {
+ memcpy(big_buffer, big_buffer + BLOCKSIZE, BLOCKSIZE);
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)big_buffer + BLOCKSIZE, BLOCKSIZE);
+#endif
+ file_recovery_new.data_check(big_buffer, 2*BLOCKSIZE, &file_recovery_new);
+ }
+ }
+ {
+ file_recovery_t file_recovery_new2;
+ file_recovery_new2.blocksize=BLOCKSIZE;
+ file_recovery_new2.file_stat=NULL;
+ file_recovery_new2.file_check=NULL;
+ file_recovery_new2.location.start=BLOCKSIZE;
+ file_recovery_new.handle=NULL; /* In theory should be not null */
+#if defined(__FRAMAC__)
+ Frama_C_make_unknown((char *)buffer, BLOCKSIZE);
+#endif
+ header_check_bmp(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2);
+ }
+ if(file_recovery_new.file_check!=NULL)
+ {
+ file_recovery_new.handle=fopen("demo", "rb");
+ if(file_recovery_new.handle!=NULL)
+ {
+ (file_recovery_new.file_check)(&file_recovery_new);
+ fclose(file_recovery_new.handle);
+ }
+ }
+ if(file_recovery_new.file_rename!=NULL)
+ {
+ /*@ assert valid_read_string((char *)&file_recovery_new.filename); */
+ (file_recovery_new.file_rename)(&file_recovery_new);
+ }
+ return 0;
+}
+#endif