recall "mode:update_mode" for efficient flow-insensitive analysis

- A user uses the mode variable in the section to define the memory
  update semantics.

- It makes the generated flow-insensitive analysis efficient.

- The user should prove the two properties to show the semantics has a
  correct use of the mode variable.

  + extensive: forall m, m <= F weak m
  + forall m, F strong m <= F weak m
Merge branch 'master' of github.com:skcho/zooberry