Compiler is unable to validate bounds

[sulekhark]

Consider the case below:

$ cat my_inet_ntop.c

#pragma CHECKED_SCOPE on

extern char *strcpy(char *restrict dest : itype(restrict _Nt_array_ptr<char>),
             const char *restrict src : itype(restrict _Nt_array_ptr<const char>))
      : itype(_Nt_array_ptr<char>);

const char *inet_ntop( char *restrict s : itype(restrict _Nt_array_ptr<char>) count(l),
        unsigned int l) : itype(_Nt_array_ptr<const char>)
{
        char buf _Nt_checked[100];
        strcpy(s, buf);
        return 0;
}

Compiler output:
$ cat my_inet_ntop_out.txt
sulekha@sulekha-VM:~/Work/checkedc-musl/build$ clang -c ../src/src/network/my_inet_ntop.c
../src/src/network/my_inet_ntop.c:11:9: warning: cannot prove argument meets declared bounds for 1st parameter [-Wcheck-bounds-decls-checked-scope]
strcpy(s, buf);
^
../src/src/network/my_inet_ntop.c:11:9: note: (expanded) expected argument bounds are 'bounds(s, s + 0)'
../src/src/network/my_inet_ntop.c:11:9: note: (expanded) inferred bounds are 'bounds(s, s + l)'
strcpy(s, buf);
^
1 warning generated.

Even when the variable l is unsigned int, the compiler is unable to prove that bounds(s, s+0) is subsumed by bounds(s, s+l).