silver
silver copied to clipboard
Improve support for Magic Wands in both backends
At the moment, Magic Wands are not entirely supported in function preconditions and in predicates. As discussed on several issues (viperproject/carbon#364, #456, viperproject/carbon#244), it was decided to disable support for such constructs until both Silicon and Carbon fully support them. A consistency check was placed in Silver in order to stop the backends from eventually crashing (viperproject/carbon#364).
Once support for Magic Wands in (at least) function preconditions and predicates is implemented, it is necessary to remove the consistency check and its respective annotations in the following test files:
- carbon/0349.vpr
- carbon/0364.vpr
- silicon/0493c.vpr
- silicon/0496.vpr
- silver/0069.vpr
- silver/0456.vpr
- new_syntax/ApplyingBranching.vpr
- new_syntax/ApplyingExpression.vpr
- new_syntax/SnapshotsWithPredicates.vpr
- regression/consistency.vpr
- regression/snapshots.vpr
- regression/wand_shapes_simple_exhale.vpr
It is also important to remove the "IgnoreFile" annotations related with the present issue.