struct fields not assignable if any are const
Steps to reproduce the issue
Consider the following C snippet:
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
produces:
$ frama-c test_global_assign.c
[kernel] Parsing test_global_assign.c (with preprocessing)
[kernel:annot-error] test_global_assign.c:9: Warning:
not an assignable left value: a.y. Ignoring logic specification of function f
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "test_global_assign.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
Expected behavior
Frama-C should accept the snippet since the y
field of a
is mutable.
Actual behaviour
Code is rejected for a.y
being non-assignable lvalue. Frama-C seems to treat the entire struct a
as const, even though only one field is declared const. Removing the const
specifier from x
causes Frama-C to accept the code.
Contextual information
23.1 (Vanadium) via opam on macOS. Does not reproduce on Frama-C 22.