Advanced Assertion Checking

[lks9]

• [x] Dependent assertions
  • [ ] Scopes for assertion labels
  • [ ] Reachability checks
  • [ ] Unique labels
• [ ] Check a single assertion on multiple traces
• [x] Debug other data while retracing (with assertions we only get true/false)
• [x] Ghost code like in JML or Frama-C
• [ ] \at( expr, label-id ) to evaluate the expression at a previous state with assertion label label-id, as in Frama-C/ACSL
• [ ] Add documentation for all above

Requires #3