Peter Goodman

Once we add jump table support to anvill, we will need to support `switch` instructions. It's also possible that they will be synthesized without our knowledge by LLVM's optimizations. McSema...

Perhaps there's a way to support this, i.e. via sequencing regions or something, where a `goto` itself is treated as some kind of black box. This is not a priority...

Repeated conditions tested in `if`? ``` + if ((int)val3 % 3 != 0U || !((int)val4 % 5 == 0U || (int)val3 % 3 != 0U)) { ```

> Question: where should it fit? Could it be that it would be easier to do that before trying to lift the bitcode, as a preprocessing step? I think doing...

This might open up opportunities. For example, if the debug info "tells" us that two LLVM values represent the same local variable, and if the two values have the same...

One thing that comes to mind is that we could feasibly treat all code as c++, but in an `extern "C"` block. Then character constants such as `'a'` would be...

We *want* to deal with those features eventually!! Like, if we had a call to `obj_msgSend` then we want to lift it to the proper AST node type.

`--remove_phi_nodes` and `--lower_switch` were used.

I would also like this explanation. For example, maybe what you're saying is that there is a place in rellic where we have the context to ask z3 about `cond`...

At least in this particular case, `!cond` and `cond` relating to a `br` instruction is valid. It's just about different interpretations of the two successors. Are there any guarantees right...