summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:30:20 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:30:20 +0100
commit410c20224cedb38a3fbae66cd1188e02bd168829 (patch)
tree9e6b237911bd964450d124bd3af76d73369256fa
parenteb2a270bfaa1fb39182dcf5622e21896afd5ec0c (diff)
src/file_pf.c: additional frama-c annotation
-rw-r--r--src/file_pf.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/file_pf.c b/src/file_pf.c
index 787a8a6..7b9a8c6 100644
--- a/src/file_pf.c
+++ b/src/file_pf.c
@@ -60,6 +60,7 @@ struct pf_header
/*@
@ requires \valid(file_recovery);
@ requires valid_read_string((char*)&file_recovery->filename);
+ @ requires file_recovery->file_rename==&file_rename_pf;
@*/
static void file_rename_pf(file_recovery_t *file_recovery)
{