My program has struct to union casting and I’m writing a checker for some of the union types. One issue I noticed is that in checkBind the SVal for the Value part seems to be lost (see sample below). Is this a known issue about casting to union? How can I get the symbol from the union casting assignment (e.g., Val → conj_$3)?
struct XY {
uint64_t X;
uint64_t Y;
};
union Pos {
struct XY xy;
};
// checkBind: Loc → xy1, Val → conj_$3{struct XY, LC1, S12330, #1}
struct xy1 = next_pos(12, 13); // implementation of next_pos is unknown to CSA
// checkBind: Loc → pos1, Val → Unknown
union Pos pos1 = (union Pos)next_pos(12, 13);