| Filename | Description |
|---|---|
| test1.vpr | Inhaling magic wand's LHS to inspect its snapshot. |
| test2.vpr | Inhaling single fields and inspect its values. |
| test3.vpr | Inhaling predicates and inspect its values. |
| test4.vpr | Inhaling fields and return some values. |
| test5.vpr | Inhaling in a method's precondition to define a magic wand's snapshot. |
| test6.vpr | Invalid inhaling leads to a inconsistent state. |
| test7.vpr | Inhaling fields with conditionals. |
| test8.vpr | Inhaling fields with value conditions. |
| test9.vpr | Inhaling does not leak any permissions. |