2.0 Release path

[pieter-bos]

Blocking issues:

• Unclear type error #917: resolve weird type errors
• Implement support for static fields and methods in the java frontend #913: static field access (test mutation, final constexpr, methods)
• String support #831: java strings
• Pointer permission syntax #836: pointer permission syntax
• Reconsider nearby-import for java #838: nearby java import
• fold/unfold inline predicates #846: fold/unfold inline predicates
• lock_invariant + default constructor #851: resolved, administrate example
• Cast to TFloat in AmbiguousPlus too optimistic #853: shape up floats a bit
• NoSuchElementException (None.get) related to inline predicates #795: inline + triggers = invalid trigger
• Make spec operators origin less lazy #814 / Lock invariant violation reported too broadly on synchronized methods #889 / Signals clause reported too broadly #890: origin of spec ops, reporting too broad
• Yields cannot access local ghost variable #837: yield target type too narrow
• CoercingRewriter is not complete yet #847: complete coercingrewriter
• ImportArray should consider the Pre-type for field generation, rather than the Post-type #848: arrays: consider pre-type for fields
• Termination support is missing error translation #876: make decreases blames
• Problems with scaling predicates #873: simplify multi-binding quantifiers
• Consistency errors with triggers #815: unsorted mess in known-problems
• Viper crash with Perm inside \let #839: let in starall

Previously blocking, but would require more extensive research:

• True matrices #791, Passing a sized array as a parameter to a C function is incorrectly interpreted by vercors #820: true matrices (needed for C, nice-to-have for multidim index expressions)
• instanceof encoding can't prove trivial assertions #827: instanceof, typing information in general
• Carbon does not optimize effectively heap-independent functions #834: heap-dependent triggers + carbon

Non-blocking issues in known-problems:

• kernel_invariant seems unsupported #852: investigate kernel_invariant
• Investigate GPGPU examples #856: generally gpgpu things seem not to work
• no-issue: mostly just unperformant examples
• Duplicate variable names are detected late and reported unclearly #547: double declarations of things
• Scale by read #769: read scaling (not required because of Value(p()) support)
• Type checking exception-related code #790: exception type checking
• Mysterious issues with monotonicBool.pvl example #819: mystery for another time
• Process models #822: process models
• Predicate families #824: predicate families
• Reducible/Contribution #826: reducible/contribution
• Java Atomics #829: atomics in java
• Vector blocks should be supported again #830: vector blocks
• Veymont examples all lack permissions to verify. Adding the permissions in the necessary places is non-trivial #840: veymont
• `fold`/`unfold` and `package`/`apply` in pure methods #842: pure fold/unfold/package/apply
• Method invocations inside while loop conditions #844: method invocations in while condition