Branch condition reporting

[marcoeilers]

Adds reporting of branch conditions to error messages when using the Silicon backend.
Here's an example:

Verification failed
Errors:
Postcondition of client_2 might not hold. Assertion (Result().value == 24) might not hold. (test_with.py@89.12--89.56).
Branch conditions: 
  (x.value > 1) at test_with.py@89.4--89.18
  (not (B() or C())) at test_with.py@90.4-90.22
  (not (unhandled exception after with)) at test_with.py@91.4--92.21
  (not (field "value" does not exist)) at test_with.py@92.8--92.21

This PR adds the Silicon option to report Viper-level branch conditions, adds Nagini code to extract and report them, and adds position and error information to a bunch of additional nodes that can be used as branch conditions but previously did not have any backtranslation information attached.

---

This change is