-extern cstring cstring_fill (cstring p_s, int p_n) /*@*/ /*@requires p_n >= 0 @*/;
-extern cstring cstring_prefix (cstring p_s, int p_n) /*@*/ /*@requires maxRead(p_s) >= p_n /\ maxSet(p_s) >= p_n @*/ /*@ensures maxRead(result) == p_n /\ maxSet(result) == p_n @*/;
-extern /*@observer@*/ cstring cstring_suffix (cstring p_s, int p_n) /*@*/ ;
+
+extern cstring cstring_fill (cstring p_s, size_t p_n) /*@*/ /*@requires p_n >= 0 @*/;
+
+extern cstring cstring_prefix (cstring p_s, size_t p_n)
+ /*@*/
+ /*@requires maxRead(p_s) >= p_n /\ maxSet(p_s) >= p_n @*/
+ /*@ensures maxRead(result) == p_n /\ maxSet(result) == p_n @*/ ;
+
+extern /*@observer@*/ cstring cstring_suffix (cstring p_s, size_t p_n) /*@*/ ;