From 9c3096c847421859958e8a5fdeab29d5eca5b3bb Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sat, 24 Oct 2020 09:05:07 +0200
Subject: [PATCH] src/file_ttf.c: Fix frama-c warnings

---
 src/file_ttf.c | 38 ++++++++++++++++++++++++++++++--------
 1 file changed, 30 insertions(+), 8 deletions(-)

diff --git a/src/file_ttf.c b/src/file_ttf.c
index be30c9ec..d0d075f7 100644
--- a/src/file_ttf.c
+++ b/src/file_ttf.c
@@ -64,9 +64,16 @@ struct ttf_table_directory
   uint32_t 	length; 	/* Length of this table. */
 };
 
+/*@
+  @ assigns \nothing;
+  @*/
 static unsigned int td_ilog2(unsigned int v)
 {
   unsigned int l = 0;
+  /*@
+    @ loop assigns v,l;
+    @ loop unroll 16;
+    @*/
   while(v >>= 1)
     l++;
   return l;
@@ -75,30 +82,45 @@ static unsigned int td_ilog2(unsigned int v)
 static int header_check_ttf(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
 {
   const struct ttf_offset_table *ttf=(const struct ttf_offset_table *)buffer;
-  unsigned int numTables;
-  numTables=be16(ttf->numTables);
+  const unsigned int numTables=be16(ttf->numTables);
+  const unsigned int entrySelector=be16(ttf->entrySelector);
+  const unsigned int searchRange=be16(ttf->searchRange);
+  const unsigned int rangeShift=be16(ttf->rangeShift);
+  if(numTables == 0)
+    return 0;
   /* searchRange 	(Maximum power of 2 <= numTables) x 16.
    * entrySelector 	Log2(maximum power of 2 <= numTables).
    * rangeShift 	NumTables x 16-searchRange.
    * */
-  if(td_ilog2(numTables) != (uint16_t)be16(ttf->entrySelector))
+  if(td_ilog2(numTables) != entrySelector)
     return 0;
-  if((16<<be16(ttf->entrySelector)) != be16(ttf->searchRange))
+  if((16<<entrySelector) != searchRange)
     return 0;
-  if(numTables * 16 != (unsigned int)be16(ttf->rangeShift)+be16(ttf->searchRange))
+  if(numTables * 16 != rangeShift+searchRange)
     return 0;
   reset_file_recovery(file_recovery_new);
   file_recovery_new->extension=file_hint_ttf.extension;
   if(sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory)
       <= buffer_size)
   {
-    const struct ttf_table_directory*ttf_dir=(const struct ttf_table_directory*)(ttf+1);
+    /*@ assert sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory) <= buffer_size; */
+    /*@ assert numTables * sizeof(struct ttf_table_directory) <= buffer_size - sizeof(struct ttf_offset_table); */
+    /*@ assert numTables <= (buffer_size - sizeof(struct ttf_offset_table)) / sizeof(struct ttf_table_directory); */
+    /*@ assert \valid_read(buffer + (0 .. buffer_size - 1)); */
+    /*@ assert \valid_read(buffer + (0 .. sizeof(struct ttf_offset_table) + numTables * sizeof(struct ttf_table_directory) - 1)); */
     uint64_t max_offset=0;
     unsigned int i;
-    for(i=0; i<numTables; i++,ttf_dir++)
+    const struct ttf_table_directory*ttf_dir=(const struct ttf_table_directory*)&buffer[sizeof(struct ttf_offset_table)];
+    /*@ assert \valid_read(ttf_dir + (0 .. numTables -1)); */
+    /*@
+      @ loop assigns i, max_offset;
+      @*/
+    for(i=0; i<numTables; i++)
     {
+      /*@ assert 0 <= i < numTables; */
+      /*@ assert \valid_read(&ttf_dir[i]); */
       /* | 0x3: align the end of the table */
-      const uint64_t new_offset=(be32(ttf_dir->offset) + be32(ttf_dir->length))|0x3;
+      const uint64_t new_offset=((uint64_t)be32(ttf_dir[i].offset) + be32(ttf_dir[i].length))|0x3;
       if(max_offset < new_offset)
 	max_offset=new_offset;
     }