search

kframework / c-semantics

Semantics of C in K
Other
303 stars 40 forks source link

Try to fix effective type of unions #624

Closed dwightguth closed 4 years ago

dwightguth commented 4 years ago

Essentially, we probably don't want to control effective typing based on the active variant of unions, because which variant is active doesn't really affect which object a pointer into the union points to... it's actually affected by which object the pointer was based on when you took the original address.

This is almost certainly not working yet, but I'm having difficulty getting the code to compile locally so I'm going to create a draft PR and examine the build result that way.

dwightguth commented 4 years ago

This solution does not work. I do not know how to make a solution that works that would not involve storing fromArray provenance in the cell, something that would likely break tons of other things in a cascading effect because of how delicate the stuff in the semantics about provenance is. It could in theory be fixed, but I'm not sure it's worth it.