Merge pull request #34 from AllanBlanchard/fix/unsigned_vs_size_t

From UINT_MAX to SIZE_MAX (or len)

code/acsl-logic-definitions/axiomatic/strlen-proved.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 
 /*@
   axiomatic StrLen {
@@ -30,7 +30,7 @@
 */
 
 /*@
-  requires valid_read_string(s) && strlen(s) <= UINT_MAX ;
+  requires valid_read_string(s) && strlen(s) <= SIZE_MAX ;
   assigns \nothing ;
   ensures \result == strlen(s) ;
 */

code/acsl-properties/lemmas/ex-2-sorted-link-answer.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+
 
 /*@ 
   predicate sorted(int* arr, integer begin, integer end) =
@@ -28,13 +28,13 @@
 
   behavior does_not_exists:
     assumes !in_array(value, arr, len);
-    ensures \result == UINT_MAX ;
+    ensures \result == len ;
 
   complete behaviors ;
   disjoint behaviors ;
 */
 size_t bsearch(int* arr, size_t len, int value){
-  if(len == 0) return UINT_MAX ;
+  if(len == 0) return len ;
 
   size_t low = 0 ;
   size_t up = len ;
@@ -52,7 +52,7 @@ size_t bsearch(int* arr, size_t len, int value){
     else if(arr[mid] < value) low = mid+1 ;
     else return mid ;
   }
-  return UINT_MAX ;
+  return len ;
 }
 
 
@@ -76,6 +76,6 @@ size_t bsearch(int* arr, size_t len, int value){
   ensures 0 <= \result < len ;
   ensures arr[\result] == value ;
 */
-unsigned bsearch_callee(int* arr, size_t len, int value){
+size_t bsearch_callee(int* arr, size_t len, int value){
   return bsearch(arr, len, value);
 }

code/acsl-properties/lemmas/ex-2-sorted-link.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+
 
 /*@ 
   predicate sorted(int* arr, integer begin, integer end) =
@@ -28,13 +28,13 @@
 
   behavior does_not_exists:
     assumes !in_array(value, arr, len);
-    ensures \result == UINT_MAX ;
+    ensures \result == len ;
 
   complete behaviors ;
   disjoint behaviors ;
 */
 size_t bsearch(int* arr, size_t len, int value){
-  if(len == 0) return UINT_MAX ;
+  if(len == 0) return len ;
 
   size_t low = 0 ;
   size_t up = len ;
@@ -52,7 +52,7 @@ size_t bsearch(int* arr, size_t len, int value){
     else if(arr[mid] < value) low = mid+1 ;
     else return mid ;
   }
-  return UINT_MAX ;
+  return len ;
 }
 
 
@@ -75,6 +75,6 @@ size_t bsearch(int* arr, size_t len, int value){
   ensures 0 <= \result < len ;
   ensures arr[\result] == value ;
 */
-unsigned bsearch_callee(int* arr, size_t len, int value){
+size_t bsearch_callee(int* arr, size_t len, int value){
   return bsearch(arr, len, value);
 }

code/acsl-properties/lemmas/ex-4-shift-transitivity-answer.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 
 /*@
   predicate shifted_cell{L1, L2}(int* p, integer shift) =
@@ -30,7 +30,7 @@
 
 /*@
   requires \valid(array+(0 .. len+shift-1)) ;
-  requires shift + len <= UINT_MAX ;
+  requires shift + len <= SIZE_MAX ;
   assigns array[shift .. shift+len-1];
   ensures shifted{Pre, Post}(array, 0, len, shift) ;
 */
@@ -49,7 +49,7 @@ void shift_array(int* array, size_t len, size_t shift){
 
 /*@
   requires \valid(array+(0 .. len+s1+s2-1)) ;
-  requires s1+s2 + len <= UINT_MAX ;
+  requires s1+s2 + len <= SIZE_MAX ;
   assigns array[s1 .. s1+s2+len-1];
   ensures shifted{Pre, Post}(array, 0, len, s1+s2) ;
 */

code/acsl-properties/lemmas/ex-4-shift-transitivity.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 
 /*@
   predicate shifted_cell{L1, L2}(int* p, integer shift) =
@@ -26,7 +26,7 @@ void shift_array(int* array, size_t len, size_t shift){
 
 /*@
   requires \valid(array+(0 .. len+s1+s2-1)) ;
-  requires s1+s2 + len <= UINT_MAX ;
+  requires s1+s2 + len <= SIZE_MAX ;
   assigns array[s1 .. s1+s2+len-1];
   ensures shifted{Pre, Post}(array, 0, len, s1+s2) ;
 */

code/acsl-properties/lemmas/ex-5-shift-sorted-answer.c

@@ -1,4 +1,4 @@
-#include <limits.h>
+#include <stdint.h>
 #include <stddef.h>
 
 /*@ 
@@ -22,13 +22,13 @@
 
   behavior does_not_exists:
     assumes !in_array(value, arr, beg, end);
-    ensures \result == UINT_MAX ;
+    ensures \result == end ;
 
   complete behaviors ;
   disjoint behaviors ;
 */
 size_t bsearch(int* arr, size_t beg, size_t end, int value){
-  if(end == beg) return UINT_MAX ;
+  if(end == beg) return end ;
 
   size_t low = beg ;
   size_t up = end ;
@@ -46,7 +46,7 @@ size_t bsearch(int* arr, size_t beg, size_t end, int value){
     else if(arr[mid] < value) low = mid+1 ;
     else return mid ;
   }
-  return UINT_MAX ;
+  return end ;
 }
 
 /*@
@@ -62,7 +62,7 @@ size_t bsearch(int* arr, size_t beg, size_t end, int value){
 
 /*@
   requires \valid(array+(0 .. len+shift-1)) ;
-  requires shift + len <= UINT_MAX ;
+  requires shift + len <= SIZE_MAX ;
   assigns array[shift .. shift+len-1];
   ensures shifted{Pre, Post}(array, 0, len, shift) ;
 */
@@ -95,7 +95,7 @@ void shift_array(int* array, size_t len, size_t shift){
 */
 
 /*@
-  requires len < UINT_MAX ;
+  requires len < SIZE_MAX ;
   requires sorted(array, 0, len) ;
   requires \valid(array + (0 .. len));
   requires in_array(value, array, 0, len) ;
@@ -104,7 +104,7 @@ void shift_array(int* array, size_t len, size_t shift){
   
   ensures 1 <= \result <= len ;
 */
-unsigned shift_and_search(int* array, size_t len, int value){
+size_t shift_and_search(int* array, size_t len, int value){
   shift_array(array, len, 1);
   return bsearch(array, 1, len+1, value);
 }

code/acsl-properties/predicates/ex-4-binary-search-answer.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+
 
 /*@ 
   predicate sorted(int* arr, integer begin, integer end) =
@@ -28,13 +28,13 @@
 
   behavior does_not_exists:
     assumes !in_array(value, arr, len);
-    ensures \result == UINT_MAX ;
+    ensures \result == len ;
 
   complete behaviors ;
   disjoint behaviors ;
 */
 size_t bsearch(int* arr, size_t len, int value){
-  if(len == 0) return UINT_MAX ;
+  if(len == 0) return len ;
 
   size_t low = 0 ;
   size_t up = len ;
@@ -52,5 +52,5 @@ size_t bsearch(int* arr, size_t len, int value){
     else if(arr[mid] < value) low = mid+1 ;
     else return mid ;
   }
-  return UINT_MAX ;
+  return len ;
 }

code/proof-methodologies/lemma-functions/ex-2-l_occurrences_of-props-answer.c

@@ -1,4 +1,4 @@
-#include <limits.h>
+#include <stdint.h>
 #include <stddef.h>
 
 /*@
@@ -118,7 +118,7 @@
         return i ;
       }
     }
-    return UINT_MAX;
+    return SIZE_MAX;
   }
 */
 

code/proof-methodologies/lemma-functions/ex-4-insert-sort.c

@@ -182,7 +182,7 @@ size_t find_last_inf(int value, int* a, size_t beg, size_t end){
 */
 
 /*@
-  requires beg < last < UINT_MAX && \valid(a + (beg .. last));
+  requires beg < last < SIZE_MAX && \valid(a + (beg .. last));
   requires sorted(a, beg, last) ;
 
   assigns a[ beg .. last ] ;
@@ -222,7 +222,7 @@ void insert(int* a, size_t beg, size_t last){
       \forall int v ;
       l_occurrences_of{Pre}(v, a, \at(i, Here), last+1) ==
         l_occurrences_of{Pre}(v, a, \at(i, Here), last) +
-	l_occurrences_of{Pre}(v, a, last, last +1);
+  l_occurrences_of{Pre}(v, a, last, last +1);
   */
 
   //@ assert rotate_left{Pre, Here}(a, i, last+1) ;
@@ -260,12 +260,12 @@ void insertion_sort(int* a, size_t beg, size_t end){
     /*@ ghost
       if(i+1 < end){
         /@ loop invariant i+1 <= j <= end ;
-	   loop invariant \forall int v ;
-	     l_occurrences_of{L}(v, a, beg, \at(j, Here)) ==
-	     l_occurrences_of(v, a, beg, j) ;
-	   loop assigns j ;
-	   loop variant end - j ;
-	@/
+           loop invariant \forall int v ;
+             l_occurrences_of{L}(v, a, beg, \at(j, Here)) ==
+             l_occurrences_of(v, a, beg, j) ;
+           loop assigns j ;
+           loop variant end - j ;
+        @/
         for(size_t j = i+1 ; j < end ; ++j);
       }
     */

code/proof-methodologies/lemma-functions/insert-sort-auto-proved.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 
 /*@
   axiomatic Occurrences_Axiomatic{
@@ -204,7 +204,7 @@ void context_to_prove_rotate_left_permutation(int* arr, size_t fst, size_t last)
 }
 
 /*@
-  requires beg < last < UINT_MAX && \valid(a + (beg .. last));
+  requires beg < last < SIZE_MAX && \valid(a + (beg .. last));
   requires sorted(a, beg, last) ;
 
   assigns a[ beg .. last ] ;

code/proof-methodologies/lemma-functions/insert-sort-auto.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 
 /*@
   axiomatic Occurrences_Axiomatic{
@@ -48,7 +48,7 @@
 */
 
 /*@
-  requires beg < last < UINT_MAX && \valid(a + (beg .. last));
+  requires beg < last < SIZE_MAX && \valid(a + (beg .. last));
   requires sorted(a, beg, last) ;
 
   assigns a[ beg .. last ] ;
@@ -99,7 +99,7 @@ void insertion_sort(int* a, size_t beg, size_t end){
     loop variant end-i ;
   */
   for(size_t i = beg+1; i < end; ++i) {
-    //@ ghost L:
+    //@ ghost L:;
     insert(a, beg, i);
     //@ assert permutation{L, Here}(a, beg, i+1);
     //@ assert unchanged{L, Here}(a, i+1, end) ;

code/proof-methodologies/lemma-functions/lemma-function-2-2.c

@@ -1,5 +1,5 @@
 #include <stddef.h>
-#include <limits.h>
+#include <stdint.h>
 /*@
   axiomatic Occurrences_Axiomatic{
     logic integer l_occurrences_of{L}(int value, int* in, integer from, integer to)
@@ -39,7 +39,7 @@
       if(in[i] == v) return i ;
     }
     /@ assert \false ; @/
-    return UINT_MAX ;
+    return SIZE_MAX ;
   }
 */
 

code/proof-methodologies/lemma-functions/lemma-macro-2-1.c

@@ -1,4 +1,4 @@
-#include <limits.h>
+#include <stdint.h>
 #include <stddef.h>
 
 /*@
@@ -12,15 +12,15 @@
 
 /*@
   requires \valid(array+(beg .. end+shift-1)) ;
-  requires shift + end <= UINT_MAX ;
+  requires shift + end <= SIZE_MAX ;
   assigns array[beg+shift .. end+shift-1];
   ensures shifted{Pre, Post}(array, beg, end, shift) ;
 */
 void shift_array(int* array, size_t beg, size_t end, size_t shift);
 
 /*@
   requires \valid(array+(0 .. len+s1+s2-1)) ;
-  requires s1+s2 + len <= UINT_MAX ;
+  requires s1+s2 + len <= SIZE_MAX ;
   assigns array[s1 .. s1+s2+len-1];
   ensures shifted{Pre, Post}(array+s1, 0, len, s2) ;
 */

code/proof-methodologies/lemma-functions/lemma-macro-2-2.c

@@ -1,4 +1,4 @@
-#include <limits.h>
+#include <stdint.h>
 #include <stddef.h>
 
 /*@
@@ -27,7 +27,7 @@ void assign_array(int* arr, size_t fst, size_t last, size_t s1, size_t s2);
 
 /*@
   requires fst <= last ;
-  requires s1+s2+last <= UINT_MAX ;
+  requires s1+s2+last <= SIZE_MAX ;
 */
 void context_to_prove_shift_ptr(int* arr, size_t fst, size_t last, size_t s1, size_t s2){
  L1: ;
@@ -43,15 +43,15 @@ void context_to_prove_shift_ptr(int* arr, size_t fst, size_t last, size_t s1, si
 
 /*@
   requires \valid(array+(beg .. end+shift-1)) ;
-  requires shift + end <= UINT_MAX ;
+  requires shift + end <= SIZE_MAX ;
   assigns array[beg+shift .. end+shift-1];
   ensures shifted{Pre, Post}(array, beg, end, shift) ;
 */
 void shift_array(int* array, size_t beg, size_t end, size_t shift);
 
 /*@
   requires \valid(array+(0 .. len+s1+s2-1)) ;
-  requires s1+s2 + len <= UINT_MAX ;
+  requires s1+s2 + len <= SIZE_MAX ;
   assigns array[s1 .. s1+s2+len-1];
   ensures shifted{Pre, Post}(array+s1, 0, len, s2) ;
 */