Checking only read permissions when asserting function preconditions

[marcoeilers]

Silver parts of the changes described here: viperproject/silicon#877

• Modify AST and ParseAST access predicates to track if a write permission was explicitly supplied or not.
• Warn whenever concrete fractions are used anywhere inside a function (done in the type checker)
• Add a command line flag to get the old behavior where permission amounts in functions are checked as usual
• Modify consistency checks to allow complex permission expressions involving wildcards in functions, so that we can allow acc(x.f, b ? wildcard : none) there, which is useful with the new interpretation but was previously forbidden. Unfortunately, this requires adding state to the Consistency object while we also support the legacy behavior.