GitLab

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.