summaryrefslogtreecommitdiffstats
path: root/src/file_tiff.h
diff options
context:
space:
mode:
authorChristophe Grenier <grenier@cgsecurity.org>2019-11-23 18:30:36 +0100
committerChristophe Grenier <grenier@cgsecurity.org>2019-11-23 18:30:36 +0100
commitb310abea46850c846c9df6cac089976c23191301 (patch)
tree265895db5165411fc78affe20b84feaf739d5da4 /src/file_tiff.h
parent7e8f99aa92038220efa4d9c45cf8a0857a77d7d8 (diff)
src/file_jpg.c: make most code frama-c friendly, file_tiff* modified to help
Diffstat (limited to 'src/file_tiff.h')
-rw-r--r--src/file_tiff.h1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/file_tiff.h b/src/file_tiff.h
index b030da2..0fb5f6c 100644
--- a/src/file_tiff.h
+++ b/src/file_tiff.h
@@ -69,7 +69,6 @@ struct ifd_header {
} __attribute__ ((gcc_struct, __packed__));
/*@
- @ requires buffer_size >= sizeof(TIFFHeader);
@ requires \valid_read(buffer+(0..buffer_size-1));
@ ensures \valid_read(buffer+(0..buffer_size-1));
@*/