Open dc-mak opened 4 months ago
That example seems to work now but this one does not:
char g(char *s);
/*@ spec g(pointer s);
requires take mi = Owned<char>(s);
ensures take mo = Owned<char>(s);
@*/
char f() {
/*@ extract Owned<char>, 0u64; @*/
return g("hello");
}
% cn verify issue_309.c
issue_309.c:8:9: warning: extract: index added, no resources (yet) extracted.
/*@ extract Owned<char>, 0u64; @*/
^~~~~~~~~~~~~~~~~~~~~~~~~~
[1/1]: f -- fail
issue_309.c:9:8: error: Missing resource for calling function g
return g("hello");
^~~~~~~~~~
Resource needed: Owned<char>(a_504)
issue_309.c:4:19: (arg mi)
a_504
is the name of the allocation containing "hello"
but this name is inaccessible to the program.
String literals are elaborated into a CreateReadOnly and this is currently not supported, so CN should warn or error on this (or implement it).