checkedc
checkedc copied to clipboard
microsoft
find-patterns.c sample code does not compile
Reading find-patterns.c I believe it is supposed to compile and run with the sample being passing lines < and > 50 characters in a line. In it's current state with the latest clang-12 implementation of checked-c the program does not compile.
check-c/spec/samples$ /home/csloaner/check-c/build/bin/clang-12 -xc --gcc-toolchain="/usr/lib/gcc/aarch64-redhat-linux/14" -L/usr/lib/gcc/aarch64-redhat-linux/14 find-pattern.c -o a.out
find-pattern.c:36:35: error: function redeclaration added bounds for parameter
int getline(char line checked[] : count(max), int max);
^
/usr/include/stdio.h:707:45: note: '__lineptr' declared here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:36:5: error: conflicting types for 'getline'
int getline(char line checked[] : count(max), int max);
^
/usr/include/stdio.h:707:18: note: previous declaration is here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:56:39: error: null terminator expected in _Nt_checked array initializer
char line nt_checked[MAXLINE + 1] = {};
^~
find-pattern.c:68:32: error: function redeclaration added bounds for parameter
int getline(char s checked[] : count(lim), int lim) {
^
/usr/include/stdio.h:707:45: note: '__lineptr' declared here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:68:5: error: conflicting types for 'getline'
int getline(char s checked[] : count(lim), int lim) {
^
/usr/include/stdio.h:707:18: note: previous declaration is here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:100:24: warning: cannot prove declared bounds for 'tmp_s' are valid after initialization [-Wcheck-bounds-decls-checked-scope]
nt_array_ptr<char> tmp_s = s + i;
~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~
find-pattern.c:100:24: note: (expanded) declared bounds are 'bounds(tmp_s, tmp_s + 0)'
find-pattern.c:100:24: note: (expanded) inferred bounds are 'bounds(s, s + i + 1)'
find-pattern.c:94:29: warning: cannot prove declared bounds for 's' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (i = 0; s[i] != '\0'; i++) {
^~~
find-pattern.c:91:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = source;
^
find-pattern.c:94:29: note: (expanded) inferred bounds are 'bounds(s, s + k + 1)'
for (i = 0; s[i] != '\0'; i++) {
^
find-pattern.c:101:58: warning: cannot prove declared bounds for 't' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^~~
find-pattern.c:92:22: note: (expanded) declared bounds are 'bounds(t, t + k)'
nt_array_ptr<char> t : count(k) = searchfor;
^
find-pattern.c:101:58: note: (expanded) inferred bounds are 'bounds(t, t + i + 1)'
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^
find-pattern.c:101:49: warning: cannot prove declared bounds for 'tmp_s' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^~~~~~~
find-pattern.c:100:24: note: (expanded) declared bounds are 'bounds(tmp_s, tmp_s + 0)'
nt_array_ptr<char> tmp_s = s + i;
^
find-pattern.c:101:49: note: (expanded) inferred bounds are 'bounds(tmp_s - 1, tmp_s - 1 + 0)'
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^
4 warnings and 5 errors generated.
-------------------------------------------------------------------------------------------------------------------------------------------------------------
check-c/spec/samples$ /home/csloaner/check-c/build/bin/clang-12 -xc find-pattern.c -o a.out
find-pattern.c:36:35: error: function redeclaration added bounds for parameter
int getline(char line checked[] : count(max), int max);
^
/usr/include/stdio.h:707:45: note: '__lineptr' declared here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:36:5: error: conflicting types for 'getline'
int getline(char line checked[] : count(max), int max);
^
/usr/include/stdio.h:707:18: note: previous declaration is here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:56:39: error: null terminator expected in _Nt_checked array initializer
char line nt_checked[MAXLINE + 1] = {};
^~
find-pattern.c:68:32: error: function redeclaration added bounds for parameter
int getline(char s checked[] : count(lim), int lim) {
^
/usr/include/stdio.h:707:45: note: '__lineptr' declared here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:68:5: error: conflicting types for 'getline'
int getline(char s checked[] : count(lim), int lim) {
^
/usr/include/stdio.h:707:18: note: previous declaration is here
extern __ssize_t getline (char **__restrict __lineptr,
^
find-pattern.c:100:24: warning: cannot prove declared bounds for 'tmp_s' are valid after initialization [-Wcheck-bounds-decls-checked-scope]
nt_array_ptr<char> tmp_s = s + i;
~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~
find-pattern.c:100:24: note: (expanded) declared bounds are 'bounds(tmp_s, tmp_s + 0)'
find-pattern.c:100:24: note: (expanded) inferred bounds are 'bounds(s, s + i + 1)'
find-pattern.c:94:29: warning: cannot prove declared bounds for 's' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (i = 0; s[i] != '\0'; i++) {
^~~
find-pattern.c:91:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = source;
^
find-pattern.c:94:29: note: (expanded) inferred bounds are 'bounds(s, s + k + 1)'
for (i = 0; s[i] != '\0'; i++) {
^
find-pattern.c:101:49: warning: cannot prove declared bounds for 'tmp_s' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^~~~~~~
find-pattern.c:100:24: note: (expanded) declared bounds are 'bounds(tmp_s, tmp_s + 0)'
nt_array_ptr<char> tmp_s = s + i;
^
find-pattern.c:101:49: note: (expanded) inferred bounds are 'bounds(tmp_s - 1, tmp_s - 1 + 0)'
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^
find-pattern.c:101:58: warning: cannot prove declared bounds for 't' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^~~
find-pattern.c:92:22: note: (expanded) declared bounds are 'bounds(t, t + k)'
nt_array_ptr<char> t : count(k) = searchfor;
^
find-pattern.c:101:58: note: (expanded) inferred bounds are 'bounds(t, t + i + 1)'
for (k = 0; t[k] != '\0' && *tmp_s == t[k]; tmp_s++, k++)
^
4 warnings and 5 errors generated.
This is being compiled on an M1 Macbook Air (aarch64) running Linux fedora 6.12.1-404.asahi.fc40.aarch64+16k #1 SMP PREEMPT_DYNAMIC Mon Dec 2 23:04:11 UTC 2024 aarch64 GNU/Linux.
string-helpers.c also does not compile while the comments suggest it should compile:
string-helpers.c:134:5: error: inferred bounds for 's' are unknown after increment
++i;
^~~
string-helpers.c:130:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = p;
^
string-helpers.c:134:7: note: lost the value of the expression 'i' which is used in the (expanded) inferred bounds 'bounds(s, s + i + 1)' of 's'
++i;
^
string-helpers.c:145:25: error: inferred bounds for 's' are unknown after increment
for ( ; s[i] != '\0'; i++) {
^~~
string-helpers.c:144:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = p;
^
string-helpers.c:145:25: note: lost the value of the expression 'i' which is used in the (expanded) inferred bounds 'bounds(s, s + i + 1)' of 's'
for ( ; s[i] != '\0'; i++) {
^
string-helpers.c:166:15: error: return used in a checked scope must have a checked type or a bounds-safe interface
for (i = 0; isspace(s[i]) && s[i] != 0; i++) // skip white space
^
/usr/include/ctype.h:197:21: note: expanded from macro 'isspace'
# define isspace(c) __isctype((c), _ISspace)
^
/usr/include/ctype.h:89:6: note: expanded from macro '__isctype'
((*__ctype_b_loc ())[(int) (c)] & (unsigned short int) type)
^
/usr/include/ctype.h:79:1: note: return declared here
extern const unsigned short int **__ctype_b_loc (void)
^
string-helpers.c:170:5: warning: cannot prove declared bounds for 's' are valid after increment [-Wcheck-bounds-decls-checked-scope]
i++;
^~~
string-helpers.c:165:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = p;
^
string-helpers.c:170:5: note: (expanded) inferred bounds are 'bounds(s, s + n + 1)'
i++;
^
string-helpers.c:172:38: error: inferred bounds for 's' are unknown after increment
for (; s[i] >= '0' && s[i] <= '9'; ++i)
^~~
string-helpers.c:165:22: note: (expanded) declared bounds are 'bounds(s, s + i)'
nt_array_ptr<char> s : count(i) = p;
^
string-helpers.c:172:40: note: lost the value of the expression 'i' which is used in the (expanded) inferred bounds 'bounds(s, s + i)' of 's'
for (; s[i] >= '0' && s[i] <= '9'; ++i)
^
string-helpers.c:184:18: error: inferred bounds for 's' are unknown after increment
for (; s[len]; len++);
^~~~~
string-helpers.c:183:22: note: (expanded) declared bounds are 'bounds(s, s + len)'
nt_array_ptr<char> s : count(len) = p;
^
string-helpers.c:184:18: note: lost the value of the expression 'len' which is used in the (expanded) inferred bounds 'bounds(s, s + len + 1)' of 's'
for (; s[len]; len++);
^~~
string-helpers.c:199:20: warning: cannot prove declared bounds for 's' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (; *s == *t; s++, t++) // Incrementing s, t allowed because *s, *t != `\0`
^~~
string-helpers.c:197:42: note: (expanded) declared bounds are 'bounds(s, s + 0)'
checked int my_strcmp(nt_array_ptr<char> s, nt_array_ptr<char> t) {
^
string-helpers.c:199:20: note: (expanded) inferred bounds are 'bounds(s - 1, s - 1 + 0)'
for (; *s == *t; s++, t++) // Incrementing s, t allowed because *s, *t != `\0`
^
string-helpers.c:199:25: warning: cannot prove declared bounds for 't' are valid after increment [-Wcheck-bounds-decls-checked-scope]
for (; *s == *t; s++, t++) // Incrementing s, t allowed because *s, *t != `\0`
^~~
string-helpers.c:197:64: note: (expanded) declared bounds are 'bounds(t, t + 0)'
checked int my_strcmp(nt_array_ptr<char> s, nt_array_ptr<char> t) {
^
string-helpers.c:199:25: note: (expanded) inferred bounds are 'bounds(t - 1, t - 1 + 0)'
for (; *s == *t; s++, t++) // Incrementing s, t allowed because *s, *t != `\0`
^
3 warnings and 5 errors generated.