Closed
Description
The const qualifier does not appear to be preserved for arrays of structs. Consider the following code:
struct foo {
int x;
float y;
};
const struct foo foo_list [3] = {
{ 1, 2.1f },
{ 2, 3.2f },
{ 3, 4.3f }
};
const int int_list[4] = {1, 2, 3, 4};
int main()
{
return 0;
}
Running through CBMC with --show-symbol-table
gives the following symbols for foo_list
and int_list
:
Symbol......: foo_list
Pretty name.: foo_list
Module......: main
Base name...: foo_list
Mode........: C
Type........: struct foo [3l]
Value.......: { { .x=1, .y=2.100000e+0f }, { .x=2, .y=3.200000e+0f }, { .x=3, .y=4.300000e+0f } }
Flags.......: lvalue static_lifetime
Location....: file main.c line 6
Symbol......: int_list
Pretty name.: int_list
Module......: main
Base name...: int_list
Mode........: C
Type........: const signed int [4l]
Value.......: { 1, 2, 3, 4 }
Flags.......: lvalue static_lifetime
Location....: file main.c line 12
The foo_list
symbol does not have the const qualifier.
Metadata
Metadata
Assignees
Labels
No labels