summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2020-06-18 18:53:39 +0200
committerChristophe Grenier <grenier@cgsecurity.org>2020-06-18 18:53:39 +0200
commitefd46ac6da9299b955ddd99acb292328411b19ee (patch)
treefb541330d07a475af75b70b858424d6c3f94bdb4
parentd895850d2f009c03fa1774ec3f63cb8e22d50793 (diff)
Fix frama-c annotation for file_allow_nl()
-rw-r--r--src/filegen.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/filegen.h b/src/filegen.h
index dc64e4e..5521ef2 100644
--- a/src/filegen.h
+++ b/src/filegen.h
@@ -123,7 +123,7 @@ void free_header_check(void);
/*@
@ requires \valid(file_recovery);
@ requires \valid(file_recovery->handle);
- @ ensures \valid(file_recovery->handle);
+ @ ensures file_recovery->handle == \old(file_recovery->handle);
@*/
void file_allow_nl(file_recovery_t *file_recovery, const unsigned int nl_mode);