Crucible panic when only one of two overrides modifies ghost state

[langston-barrett]

test_ghost_branch_02 in #541 causes Crucible to panic. The gist is that the function f modifies an external global variable (modeled with ghost state) in only one of its two branches. Accordingly, f has two overrides, one where the ghost state gets mutated, and one where it doesn't. If these branches are merged, then the panic occurs.

Quoting from a conversation with @brianhuffman:

That message means that there is a global variable that exists in one branch, but does not exist at all in the other branch. This is not supposed to happen, because you are only supposed to create new global variables at the top-level, and not while inside a branch
It would be better if we would detect that problem when the global is created, instead of later when the merge happens
The reason for the restriction is that global variables are supposed to contain defined values, never partial values. Merging an existing value with a non-existing one would require creating a partial value
Maybe it should declare the other kind of variable instead, by which I mean a RefCell as opposed to a GlobalVar. See module Lang.Crucible.Simulator.GlobalState in package crucible

TL;DR: Ghost state is modeled using Crucible's global variables, it probably shouldn't be due to inherent restrictions on having different sets of globals in different branches.

[atomb]

It looks like test_ghost_branch_02 is succeeding now, so I'm going to close this.