Closed
Description
Const qualifiers seem to be lost on tagged structs and unions. Consider the following code:
struct struct_tag_name
{
int x;
float y;
};
int main()
{
const struct struct_tag_name my_struct_var = {.x = 1, .y = 3.15};
const double z = 4;
return 0;
}
In the symbol table for the compiled GOTO program, you get the following symbols for the two variables in main
:
Symbol......: main::1::my_struct_var
Pretty name.: main::1::my_struct_var
Module......: main
Base name...: my_struct_var
Mode........: C
Type........: struct struct_tag_name
Value.......: { .x=1, .y=(float)3.150000e+0 }
Flags.......: lvalue thread_local file_local
Location....: file main.c line 10 function main
Symbol......: main::1::z
Pretty name.: main::1::z
Module......: main
Base name...: z
Mode........: C
Type........: const double
Value.......: (const double)4
Flags.......: lvalue thread_local file_local
Location....: file main.c line 11 function main
Note z
's type is correctly marked as a const double
but my_struct_var
only has type struct struct_tag_name
.
This happens independently of whether you run goto-cc then goto-instrument or run the file straight through cbmc.
Metadata
Metadata
Assignees
Labels
No labels