Extend parser for specifications to support read permissions

As an example, consider the list_copy specification:

{ r :-> x ** lseg(x, S) }
  void listcopy(loc r)
{ r :-> y ** lseg(x, S) ** lseg(y, S) }

It would be nice to be able to state something like

{ r :-> x ** [lseg(x, S)] }

in the precondition to indicate that this lseg is not to be unfolded during the synthesis. In the future, the syntax may be enhanced with fractional permissions.

This issue is about AST/parsing only. It does not cover the semantics of read-only permissions.