summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:17:42 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:17:42 +0200
commit4e5978cf5f7ff8ba346adec469cf3658ed19b00d (patch)
tree5640a799ee8afac6c1fb236d3d18c185ac226f95
parenta43423c2badcc38c3843556558706d26601d7cfe (diff)
Fix the remaining problems reported by "make frama-c-bmp" and "make frama-c-doc"
-rw-r--r--src/file_bmp.c9
-rw-r--r--src/file_doc.c9
2 files changed, 12 insertions, 6 deletions
diff --git a/src/file_bmp.c b/src/file_bmp.c
index 340a1c6..42209d2 100644
--- a/src/file_bmp.c
+++ b/src/file_bmp.c
@@ -105,6 +105,9 @@ static int header_check_bmp(const unsigned char *buffer, const unsigned int buff
return 0;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
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);
@@ -114,7 +117,7 @@ static void register_header_check_bmp(file_stat_t *file_stat)
#define BLOCKSIZE 65536u
int main()
{
- const char *fn = "recup_dir.1/f0000000.bmp";
+ const char fn[] = "recup_dir.1/f0000000.bmp";
unsigned char buffer[BLOCKSIZE];
int res;
file_recovery_t file_recovery_new;
@@ -144,8 +147,8 @@ int main()
register_header_check_bmp(&file_stats);
if(header_check_bmp(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1)
return 0;
- /*@ assert valid_read_string(fn); */
- strcpy(file_recovery_new.filename, fn);
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
file_recovery_new.file_stat=&file_stats;
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
/*@ assert file_recovery_new.extension == file_hint_bmp.extension; */
diff --git a/src/file_doc.c b/src/file_doc.c
index d58f138..de28d49 100644
--- a/src/file_doc.c
+++ b/src/file_doc.c
@@ -1430,6 +1430,9 @@ static void file_rename_doc(file_recovery_t *file_recovery)
file_rename(file_recovery, NULL, 0, 0, ext, 1);
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_doc(file_stat_t *file_stat)
{
static const unsigned char doc_header[]= { 0xd0, 0xcf, 0x11, 0xe0, 0xa1, 0xb1, 0x1a, 0xe1};
@@ -1440,7 +1443,7 @@ static void register_header_check_doc(file_stat_t *file_stat)
#define BLOCKSIZE 65536u
int main()
{
- const char *fn = "recup_dir.1/f0000000.doc";
+ const char fn[] = "recup_dir.1/f0000000.doc";
unsigned char buffer[BLOCKSIZE];
file_recovery_t file_recovery_new;
file_recovery_t file_recovery;
@@ -1474,8 +1477,8 @@ int main()
#ifdef __FRAMAC__
file_recovery_new.file_size = 512*Frama_C_interval(1, 1000);
#endif
- /*@ assert valid_read_string(fn); */
- strcpy(file_recovery_new.filename, fn);
+ /*@ assert valid_read_string((char *)&fn); */
+ memcpy(file_recovery_new.filename, fn, sizeof(fn));
/*@ assert valid_read_string((char *)&file_recovery_new.filename); */
/*@ assert valid_read_string((char *)file_recovery_new.filename); */
file_recovery_new.file_stat=&file_stats;