The initial constraint on the program analysed is given in a logic which is a restriction of the CSL logic defined in [Bouajjani and al. CONCUR-09]. This logic is a multi-sorted first order logic with reachability predicates. More precisely, in this logic one can use the following terms:
n, i.e., the number of edges of the segment.
data[n]in the multiset constraints.
The atomic constraints of the logic are the following:
xis labeling a node of a heap called
xlabels a node from which starts a segment which is acyclic.
xlabels a node from which starts a segment which reaches another node labeled by
xlabels a node from which starts a segment which is disjoint from (does not share nodes with) the list segment which starting node is labeled by