summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:31:13 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-12-07 20:31:13 +0100
commitded0ae6ed77785c6899f33194fa9d145c5e2dad1 (patch)
tree4d6fdc8fbc866793d4044bec222470b7810101f1
parent1f77cbec99dcfe25d7a1d951fed82f5344d95de7 (diff)
file_tiff*: additional frama-c annotations
-rw-r--r--src/file_tiff.h1
-rw-r--r--src/file_tiff_be.c1
2 files changed, 2 insertions, 0 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index 0fb5f6c..51059f5 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -99,6 +99,7 @@ unsigned int find_tag_from_tiff_header_le(const unsigned char *buffer, const uns
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
+ @ requires fr->file_check==&file_check_tiff_le;
@ ensures \valid(fr->handle);
@ ensures valid_read_string(fr->extension);
@*/
diff --git a/src/file_tiff_be.c b/src/file_tiff_be.c
index 92ac870..dfe17a3 100644
--- a/src/file_tiff_be.c
+++ b/src/file_tiff_be.c
@@ -659,6 +659,7 @@ static uint64_t file_check_tiff_be_aux(file_recovery_t *fr, const uint32_t tiff_
@ requires \valid(fr->handle);
@ requires \valid_read(&fr->extension);
@ requires valid_read_string(fr->extension);
+ @ requires fr->file_check==&file_check_tiff_be;
@*/
static void file_check_tiff_be(file_recovery_t *fr)
{