diff options
Diffstat (limited to 'src/unicode.c')
| -rw-r--r-- | src/unicode.c | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/unicode.c b/src/unicode.c index b499ac2b..304cb3b6 100644 --- a/src/unicode.c +++ b/src/unicode.c @@ -31,6 +31,10 @@ int UCSle2str(char *to, const uint16_t *from, const unsigned int len) { unsigned int i; + /*@ + @ loop assigns i, to[0 .. i]; + @ loop variant len - i; + @*/ for (i = 0; i < len && le16(from[i])!=0; i++) { if (le16(from[i]) & 0xff00) @@ -46,6 +50,10 @@ int UCSle2str(char *to, const uint16_t *from, const unsigned int len) int str2UCSle(uint16_t *to, const char *from, const unsigned int len) { unsigned int i; + /*@ + @ loop assigns i, to[0 .. i]; + @ loop variant len - i; + @*/ for (i = 0; (i < len) && from[i]; i++) { to[i] = le16(from[i]); |