Adapt to effective types checks for pointer vars

Fixes two cases where the tutorial was not compliant with
VeriFast's new checks for compliance with C's effective types
rules when accessing variables of pointer type (see
verifast/verifast#542).

Update tutorial after VeriFast breaking changes

In particular, the recent changes to VeriFast that introduce the
distinction between predicates representing initialized memory
(e.g. account_balance) and predicates representing
possibly-uninitialized memory (e.g. account_balance_)
necessitate a number of small changes to the tutorial.