search

kframework / c-semantics

Semantics of C in K
Other
306 stars 41 forks source link

fix nested union bug #613

Closed h0nzZik closed 4 years ago

h0nzZik commented 4 years ago

This fixes the union bug reported by Denso.

dwightguth commented 4 years ago

Can you describe in english exactly what this change is doing?

h0nzZik commented 4 years ago

Previously, when the outer union did not contain the given member (j for the accompanying test), the original rule did not apply - no rule for union applied, and therefore the [owise] rule applied, which was a problem. I relaxed restrictions on that rule such that in applied in that case, but kept the guard strong enough so that it cannot fire when the rule below (the one with calls to getUnnamed, which probably handles the case of anonymous union member) is enabled. Note that the first line of the modified guard:

(notBool isNoType(getFieldType(F, T)) orBool isNoType(findFieldType(F, T)))

is exactly a negation of the guard from the second rule:

isNoType(getFieldType(F, T)) andBool notBool isNoType(findFieldType(F, T))