summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:22:43 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2019-10-19 10:22:43 +0200
commit574c1938aee10763109d92e82592544e5d422c56 (patch)
tree9e1f94877d22201dce7e008c958c66c43852a2b2
parent672e4ff620abb0dd817f92f421511dda96262868 (diff)
Fix the remaining problems reported by "make frama-c-pf"
-rw-r--r--src/file_pf.c9
1 files changed, 6 insertions, 3 deletions
diff --git a/src/file_pf.c b/src/file_pf.c
index 68dac3c..787a8a6 100644
--- a/src/file_pf.c
+++ b/src/file_pf.c
@@ -105,6 +105,9 @@ static int header_check_pf(const unsigned char *buffer, const unsigned int buffe
return 1;
}
+/*@
+ @ requires \valid(file_stat);
+ @*/
static void register_header_check_pf(file_stat_t *file_stat)
{
static const unsigned char pf_header[7] = {0x00, 0x00, 0x00, 'S', 'C', 'C', 'A'};
@@ -115,7 +118,7 @@ static void register_header_check_pf(file_stat_t *file_stat)
#define BLOCKSIZE 65536u
int main()
{
- const char *fn = "recup_dir.1/f0000000.pf";
+ const char fn[] = "recup_dir.1/f0000000.pf";
unsigned char buffer[BLOCKSIZE];
file_recovery_t file_recovery_new;
file_recovery_t file_recovery;
@@ -143,8 +146,8 @@ int main()
register_header_check_pf(&file_stats);
if(header_check_pf(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));
/*@ assert file_recovery_new.file_size == 0; */
/*@ assert file_recovery_new.extension == file_hint_pf.extension; */
/*@ assert file_recovery_new.file_rename==&file_rename_pf; */