Contract

We currently support the following contract inference:

Return values

• for Pointers, derive the pset from parameters
• for Aggregate, expand it and derived the pset of pointer sub-objects from parameters

Note: only single-level pointer is supported, eg. T*, not T**.

Parameters

• for pointers to value, value will not be expanded
• for pointers to owner, as the paper
• for pointers to pointers ,as the paper
• for pointers to aggregate, aggregate will be expanded, but only single-level pointers will be derived
• for aggregates, expand it, but only single-level pointers will be derived, pointers to owners/pointers are not derived