summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
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 /src/file_tiff.h
parent1f77cbec99dcfe25d7a1d951fed82f5344d95de7 (diff)
file_tiff*: additional frama-c annotations
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h1
1 files changed, 1 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);
@*/