Should string literals be const, like in C++?

[mlbrooks]

With array type:

#ifndef __cforall
#include <stdio.h>
#endif

int main(int argc, char ** argv) {
    char s[] = "hello";
    s[3] = 'p';
    s[4] = '!';
    printf("%s\n", s);
}

gcc actual, g++ actual, cfa actual: compile succeeds, run prints "help!"

With pointer type:

#ifndef __cforall
#include <stdio.h>
#endif

int main(int argc, char ** argv) {
    char *s = "hello";
    s[3] = 'p';
    s[4] = '!';
    printf("%s\n", s);
}

gcc actual, cfa actual: compile succeeds, run gets segmentation fault

g++ actual: compiler warning, ISO C++ forbids converting a string constant to 'char*'

[ajbeach]

I vote for this. The only downside is C->CFA code might require adding const in a few more places but only in places where it helps anyways.

[ajbeach]

I discovered a problem as I tried to implement this.

We have been handling pointer initialization and array initialization the same. They are implemented differently, but only at the C level so we just package up the code and move it through the same lines. However, this change has made one of the significant differences between the two forms of initialization come up.

And that is initializing a pointer to mutable from a pointer to constant is invalid (because that would allow you to write to the constant) but initializing an array of mutable from an array of constant is fine (because those constants are copied over into new storage). This is a case where we must consider the fact the underlying storage of these two types is different.