src/common.[ch]: improve Frama-C annotations

2 files changed, 32 insertions, 10 deletions

diff --git a/src/common.c b/src/common.c
index 3b3a3cae..c37bddd0 100644
--- a/src/common.c
+++ b/src/common.c
@@ -192,32 +192,42 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
 {
   unsigned int i;
   /*@
-    @ loop assigns i, partition->fsname[i];
+    @ loop invariant \separated(partition, src + (..));
     @ loop invariant 0 <= i < sizeof(partition->fsname);
     @ loop invariant 0 <= i <= max_size;
+    @ loop invariant \initialized(partition->fsname+(0 .. i-1));
+    @ loop assigns i, partition->fsname[0 .. i];
+    @ loop variant sizeof(partition->fsname)-1 - i;
     @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
   partition->fsname[i]='\0';
+  /*@ assert valid_string((char *)&partition->fsname); */
 }
 
 void set_part_name_chomp(partition_t *partition, const char *src, const unsigned int max_size)
 {
   unsigned int i;
   /*@
-    @ loop assigns i, partition->fsname[i];
+    @ loop invariant \separated(partition, src + (..));
     @ loop invariant 0 <= i < sizeof(partition->fsname);
     @ loop invariant 0 <= i <= max_size;
+    @ loop invariant \initialized(partition->fsname+(0 .. i-1));
+    @ loop assigns i, partition->fsname[0 .. i];
+    @ loop variant sizeof(partition->fsname)-1 - i;
     @*/
   for(i=0; i<sizeof(partition->fsname)-1 && i<max_size && src[i]!='\0'; i++)
     partition->fsname[i]=src[i];
   /*@
-    @ loop assigns i;
     @ loop invariant 0 <= i < sizeof(partition->fsname);
+    @ loop invariant \initialized(partition->fsname+(0 .. i-1));
+    @ loop assigns i;
+    @ loop variant i;
     @*/
   while(i>0 && partition->fsname[i-1]==' ')
     i--;
   partition->fsname[i]='\0';
+  /*@ assert valid_string((char *)&partition->fsname); */
 }
 
 char* strip_dup(char* str)
@@ -453,8 +463,9 @@ int check_command(char **current_cmd, const char *cmd, const size_t n)
 void skip_comma_in_command(char **current_cmd)
 {
   /*@
-    loop invariant valid_read_string(*current_cmd);
-    loop assigns *current_cmd;
+    @ loop invariant valid_read_string(*current_cmd);
+    @ loop assigns *current_cmd;
+    @ loop variant strlen(*current_cmd);
     */
   while(*current_cmd[0]==',')
   {
@@ -467,9 +478,10 @@ uint64_t get_int_from_command(char **current_cmd)
 {
   uint64_t tmp=0;
   /*@
-    loop invariant valid_read_string(*current_cmd);
-    loop assigns *current_cmd, tmp;
-    */
+    @ loop invariant valid_read_string(*current_cmd);
+    @ loop assigns *current_cmd, tmp;
+    @ loop variant strlen(*current_cmd);
+    @*/
   while(*current_cmd[0] >='0' && *current_cmd[0] <= '9')
   {
 #ifdef __FRAMAC__
diff --git a/src/common.h b/src/common.h
index 6e643783..3b2397a4 100644
--- a/src/common.h
+++ b/src/common.h
@@ -529,7 +529,9 @@ void *MALLOC(size_t size);
   @ requires \valid(partition);
   @ requires valid_partition(partition);
   @ requires \valid_read(src + (0 .. max_size-1));
-  @ requires \separated(partition, src);
+  @ requires \separated(partition, src + (..));
+  @ terminates \true;
+  @ ensures valid_string((char *)&partition->fsname);
   @*/
 void set_part_name(partition_t *partition, const char *src, const unsigned int max_size);
 
@@ -538,11 +540,14 @@ void set_part_name(partition_t *partition, const char *src, const unsigned int m
   @ requires valid_partition(partition);
   @ requires \valid_read(src + (0 .. max_size-1));
   @ requires \separated(partition, src);
+  @ terminates \true;
+  @ ensures valid_string((char *)&partition->fsname);
   @*/
 void set_part_name_chomp(partition_t *partition, const char *src, const unsigned int max_size);
 
 /*@
   @ requires valid_read_string(str);
+  @ terminates \true;
   @ ensures \result == \null || valid_read_string(\result);
   @*/
 char* strip_dup(char* str);
@@ -556,7 +561,10 @@ time_t date_dos2unix(const unsigned short f_time,const unsigned short f_date);
 
 void set_secwest(void);
 
-/*@ assigns \nothing; */
+/*@
+  @ terminates \true;
+  @ assigns \nothing;
+  @*/
 time_t td_ntfs2utc (int64_t ntfstime);
 #ifndef BSD_MAXPARTITIONS
 #define	BSD_MAXPARTITIONS	8
@@ -649,6 +657,7 @@ struct tm *localtime_r(const time_t *timep, struct tm *result);
   @ requires valid_read_string(cmd);
   @ requires \separated(cmd+(..), current_cmd, *current_cmd);
   @ requires strlen(cmd) == n;
+  @ terminates \true;
   @ assigns  *current_cmd;
   @ ensures  valid_read_string(*current_cmd);
   @ ensures  \result != 0 ==> *current_cmd == \old(*current_cmd);
@@ -670,6 +679,7 @@ void skip_comma_in_command(char **current_cmd);
   @ requires \valid(current_cmd);
   @ requires valid_read_string(*current_cmd);
   @ requires \separated(current_cmd, *current_cmd);
+  @ terminates \true;
   @ assigns  *current_cmd;
   @ ensures  valid_read_string(*current_cmd);
   @*/