| Issue 42: | Reference equality invariants / method pre-/post-conditions | |
| Back to list |
Support for invariants like "head==tail", maybe even for method pre-/post-conditions. Local alias analysis should be able to do this, except is currently separate from the actual permission analysis and would probably have to be integrated. |