Make IL control-flow representation match boogie more closely

[ailrst]

The IL should represent conditional calls, and branching, closer to boogie. This means removing conditions from DirectCalls and replacing them with an assume preceding the call.

E.g.

                        ┌─────────────┐
                        │ statement1  │
                        │ statement2  │
                        │ ----------  │
                        │ goto a      │
                        │ goto b      │
              ┌─────────┴─────────────┴───────────┐
              │                                   │
 ┌────────────▼───────────┐        ┌──────────────▼─────────┐
 │a:assume R0 == 699900   │        │b:assume R0 == 699908   │
 │ --------------------   │        │ ---------------------- │
 │ DirectCall(ProcedureA) │        │ DirectCall(ProcedureB) │
 └────────────────────────┴────┬───┴────────────────────────┘
                               │
                        ┌──────▼──────┐
                        │ statement3  │
                        │ statement4  │
                        │ ----------  │
                        │ goto c      │
                        └─────────────┘

[l-kent]

It's GoTos that we would want to remove the conditions from, not DirectCalls (I have already removed conditions from DirectCalls in changes for #132 that are not yet pushed).