Extend graphOf to handle all stmts; complete iteration property proof

graphOf fails (returns NONE) when it encounters a Malloc statement.
I think this is reasonable given that we're applying graphOf to
executors, not inspectors.
Proof progress; checking in to transfer code from machine to machine.