using the “emptiness markers” condition of $s^1 \sqsubseteq^\text{Seg} s^2$ for all the indices $k$ such that $\phi^{3\to2}(i-1) < k \le \phi^{3\to2}(i)$, we know that for every one of those indices $k$ we have

$$ \left( \bigwedge_{j=\phi^{2\to1}(k-1)+1}^{\phi^{2\to1}(k)} m_j^1 \right) \Rightarrow m_k^2 $$

Additionally, using the “emptiness markers” condition of $s^2 \sqsubseteq^\text{Seg} s^3$ at index $i$, we know that

$$ \left( \bigwedge_{k=\phi^{3\to2}(i-1)+1}^{\phi^{3\to2}(i)} m_k^2 \right) \Rightarrow m_i^3 $$

Hence,

$$ \left( \bigwedge_{j=\phi(i-1)+1}^{\phi(i)} m_j^1 \right) \Rightarrow \left( \bigwedge_{k=\phi^{3\to2}(i-1)+1}^{\phi^{3\to2}(i)} m_k^2 \right) \Rightarrow m_i^3 $$

□

## Unification of segmentations

In order to more easily define the two operations used during unification (boundset splitting and bound expression removal), we are going to introduce two notations on sequences: sequence slicing and sequence concatenation. If $\sigma$ is a sequence, then $\sigma[i:j]$ is the sequence that contains the elements of $\sigma$ between indices $i$ and $j$. If $\sigma_1$ and $\sigma_2$ are two sequences, then $\sigma_1 \cdot \sigma_2$ is the concatenation of $\sigma_1$ and $\sigma_2$.

**Definition 37 (Boundset splitting).** For any segmentation $s = (l, v, b_0, \sigma)$, with a sequence of segments $\sigma = (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}$, any segmentation index $i_0 \in \{0, \dots, n\}$, any two non-empty boundsets $b^1$ and $b^2$ that form a partition of $b_{i_0}$, and any segment summary $d_0$ the splitting of $s$ at index $i_0$ on boundsets $b^1$ and $b^2$ with summary $d_0$ is the segmentation defined by

$$ \text{Split}(s, i_0, b^1, b^2, d_0) = \begin{cases} (l, v, b^1, (d_0, b^2, \mathfrak{t}) \cdot \sigma) & \text{if } i_0 = 0 \\ (l, v, b_0, \sigma[1: i_0 - 1] \cdot \sigma' \cdot \sigma[i_0 + 1:n]) & \text{if } i_0 \neq 0 \\ \text{where } \sigma' = (d_{i_0}, b^1, m_{i_0}) \cdot (d_0, b^2, \mathfrak{t}) & \text{if } i_0 = 1 \end{cases} $$

Splitting a boundset amounts to relaxing an equality constraint, which explains why the result is less precise.

**Lemma 8 (Boundset splitting yields a value less precise than the initial one).** For any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}})$, any segmentation index $i_0 \in \{0, \dots, n\}$, any two non-empty boundsets $b^1$ and $b^2$ that form a partition of $b_{i_0}$, and any segment summary $d_0$ such that $d_0 \sqsubseteq^\text{SL} d_{i_0}$, we have

$$ s \sqsubseteq^\text{Seg} \text{Split}(s, i_0, b^1, b^2, d_0) $$

When defining the removal of bound expressions from a segmentation, we proceed in two steps, by first defining how to remove them at a particular index, and then defining the same operation for all indices at once.
**Definition 38** (Bound expression removal). For any segmentation $s = (l, v, b_0, \sigma)$, with a sequence of segments $\sigma = (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}$, any set of bound expressions $b$ and any segmentation index $i_0 \in \{0, \dots, n\}$, the removal of bound expressions $b$ from segmentation $s$ at index $i_0$ is given by

$$ \text{RemBexpAtIndex}(b, s, i_0) = \begin{cases} (l, v, b_0 \setminus b, \sigma) & \text{if } i_0 = 0 \\ (l, v, b_0, \sigma[1 : i_0 - 1] \cdot (d_{i_0}, b_{i_0} \setminus b, m_{i_0}) \cdot \sigma[i_0 + 1 : n]) & \text{if } b_{i_0} \setminus b \neq \emptyset \\ (l, v, b_0, \sigma[1 : i_0 - 1] \cdot (d_{i_0} \sqcup^S d_{i_0+1}, b_{i_0+1}, m_{i_0} \wedge m_{i_0+1}) \cdot \sigma[i_0 + 2 : n]) & \text{if } b_{i_0} \setminus b = \emptyset \end{cases} $$

Then, the removal of bound expressions $b$ from segmentation $s$ is given by

$$ \text{RemoveBexp}(b, s) = \text{RemBexpAtIndex}(b, \dots, \text{RemBexpAtIndex}(b, s, 0), \dots, n) $$

In order to keep well-formed segmentations, we do not allow removing the constant 0 from $b_0$, nor the length variable from $b_n$. This ensures that the cases where $b_{i_0} \setminus b = \emptyset$ with $i_0 = 0$ or $i_0 = n$ are not possible. Removing bound expressions amounts to relaxing equality and inequality constraints. Which is why the result is less precise.

**Lemma 9** (Bound expression elimination yields a value less precise than the initial one). For any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}})$ and any set of bound expressions $b$,

$$ s \sqsubseteq^{\text{Seg}} \text{RemoveBexp}(b, s) $$

Here, segment-wise operations on unified segmentations are written with an over-line:

**Definition 39** (Segment-wise operations). For any two unified segmentations $s^1 = (l, v, b_0, (d_i^1, b_i, m_i^1)_{i \in \{1, \dots, n\}})$ and $s^2 = (l, v, b_0, (d_i^2, b_i, m_i^2)_{i \in \{1, \dots, n\}})$ union, intersection and widening are defined as follows:

$$ \begin{aligned} s^1 \sqcup^{\text{Seg}} s^2 &= (l, v, b_0, (d_i^1 \sqcup^S d_i^2, b_i, m_i^1 \vee m_i^2)_{i \in \{1, \dots, n\}}) \\ s^1 \sqsupseteq^{\text{Seg}} s^2 &= (l, v, b_0, (d_i^1 \sqcap^S d_i^2, b_i, m_i^1 \wedge m_i^2)_{i \in \{1, \dots, n\}}) \\ s^1 \sqsupseteq^{\text{Seg}} s^2 &= (l, v, b_0, (d_i^1 \sqsupset^S d_i^2, b_i, m_i^1 \vee m_i^2)_{i \in \{1, \dots, n\}}) \end{aligned} $$

**Lemma 10** (Soundness of segment-wise operations). The segment-wise operations are sound on unified segmentations:

* If $s_1$ and $s_2$ are two unified segmentations, then

$$ \gamma^{\text{Seg}}(s_1) \cup \gamma^{\text{Seg}}(s_2) \subseteq \gamma^{\text{Seg}}(s_1 \sqcup^{\text{Seg}} s_2) $$

* If $s_1$ and $s_2$ are two unified segmentations, then

$$ \gamma^{\text{Seg}}(s_1) \cap \gamma^{\text{Seg}}(s_2) \subseteq \gamma^{\text{Seg}}(s_1 \sqcap^{\text{Seg}} s_2) $$
* The widening $\overline{\nabla}^{\text{seg}}$ computes upper-bounds on unified segmentations. If $s_1$ and $s_2$ are two unified segmentations, then

$$s_1 \sqsubseteq^{\text{Seg}} s_1 \overline{\nabla}^{\text{seg}} s_2$$

$$s_2 \sqsubseteq^{\text{Seg}} s_1 \overline{\nabla}^{\text{seg}} s_2$$

* Widening enforces convergence in finite time. If $(s_i)_{i \in \mathbb{N}}$ is a sequence of unified segmentations, then the sequence $(s'_i)_{i \in \mathbb{N}}$ defined by $s'_0 = s_0$ and, for all $n \in \mathbb{N}$, $s'_{n+1} = s'_n \overline{\nabla}^{\text{disj}} s_{n+1}$, then there exists an index $n_0 \in \mathbb{N}$ such that, for any $n \ge n_0$, we have $s'_n = s'_{n_0}$.

**Proof that segment-wise union is sound on unified segmentations.** Let $s^1 = (l, v, b_0^1, (d_i^1, b_i^1, m_i^1)_{i \in \{1, \dots, n\}})$ and $s^2 = (l, v, b_0^2, (d_i^2, b_i^2, m_i^2)_{i \in \{1, \dots, n\}})$ be two unified segmentations. Let $(\rho, t) \in \gamma^{\text{Seg}}(s^1) \cup \gamma^{\text{Seg}}(s^2)$ be an environment-array pair in the concretisation of either $s^1$ or $s^2$. The definition of $s^1 \sqsubseteq^{\text{seg}} s^2$ being symmetric on $s^1$ and $s^2$, we can assume without loss of generality that $(\rho, t) \in \gamma^{\text{Seg}}(s^1)$. The goal is to prove that $(\rho, t) \in \gamma^{\text{Seg}}(s^1 \sqsubseteq^{\text{seg}} s^2)$. In order to prove that, we need to check the five conditions of Definition 32. Since the boundsets of $s^1 \sqsubseteq^{\text{seg}} s^2$ are exactly the same ones of $s^1$, the “Equalities in each boundset”, “Inequalities between boundsets” and “Array size” conditions stem directly from $(\rho, t) \in \gamma^{\text{Seg}}(s^1)$. The conditions that are left to verify are “Strict inequalities for non-empty segments” (which involves emptiness markers) and “Segment summaries” (which involves segment summaries). We write $s' = (l, v, b_0, (d'_i, b_i, m'_i)_{i \in \{1, \dots, n\}})$ for the segmentation $s^1 \sqsubseteq^{\text{seg}} s^2$.

**Strict inequalities for non-empty segments.** Let $i \in \{1, \dots, n\}$ be an index of segmentation $s'$. For this condition, we get to assume that $m'_i$ is false, and we need to show that $[[b_{i-1}]_{\rho}^{\text{exp}}] < [[b_i]_{\rho}^{\text{exp}}]$. By definition, we have $m'_i = m_i^1 \lor m_i^2$. Hence, since $m'_i$ is false, we know that $m_i^1$ and $m_i^2$ are both false. By using the “Strict inequalities for non-empty segments” property from $(\rho, t) \in \gamma^{\text{Seg}}(s^1)$ we have the desired inequality: $[[b_{i-1}]_{\rho}^{\text{exp}}] < [[b_i]_{\rho}^{\text{exp}}]$.

**Segment summaries.** Let $i \in \{1, \dots, n\}$ be a segment index and $j$ be an array index for that segment (that is, such that $[[b_{i-1}]_{\rho}^{\text{exp}}] \le j < [[b_i]_{\rho}^{\text{exp}}]$). The goal here is to prove that the environment $\rho$ extended with value $j$ for variable $l$ and value $t[j]$ for variable $v$, belongs to the concretisation of $d'_i = d_i^1 \sqcup^S d_i^2$. In other words, the goal is to prove $\rho[l \mapsto j][v \mapsto t[j]] \in \gamma^{\text{S}}(d'_i)$. Using the “Segment summaries” condition from $(\rho, t) \in \gamma^{\text{Seg}}(s^1)$, we have $\rho[l \mapsto j][v \mapsto t[j]] \in \gamma^{\text{Seg}}(d_i^1)$. Then, using the soundness of $\sqcup^S$, we have that $\gamma^{\text{S}}(d_i^1) \cup \gamma^{\text{S}}(d_i^2) \subseteq \gamma^{\text{S}}(d_i^1 \sqcup^S d_i^2)$; hence in particular $\rho[l \mapsto j][v \mapsto t[j]] \in \gamma^{\text{S}}(d_i^1 \sqcup^S d_i^2) = \gamma^{\text{S}}(d'_i)$. $\square$

The proofs for intersection and widening use similar arguments.

For intersection, union and widening, we use the same unification algorithm as [12]. We refer the reader to section 11.4 of [12] for details.

## A.1.2 Array environments

For a typing context $\Gamma$, we recall that $\text{Arr}(\Gamma)$ is the set of variables that have an array type.

The domain for abstracting arrays is defined by associating a segmentation to each variable that has an array type.
**Definition 40 (Abstract array environments).** For any numeric domain N, we define a domain for arrays, written A(N). For any typing context Γ, the elements $a \in A(N)(\Gamma) = \prod_{x \in \text{Arr}(\Gamma)} \text{Seg}(N)(\Gamma)(x)$ of the domain for arrays are called abstract array environments, and they associate, to every variable $x \in \text{Arr}(\Gamma)$ with an array type, a segmentation $a(x) \in \text{Seg}(N)(\Gamma)(x)$.

**Definition 41 (Concretisation for abstract array environments).** The concretisation for abstract array environments $\gamma^A$ is defined by:

$$ \gamma^A(a) = \{ \rho \mid \forall x \in \text{Arr}(\Gamma), (\rho, \rho(x)) \in \gamma^{\text{Seg}}(a(x)) \} $$

All operations on abstract array environments (pre-order, intersection, union and widening) are performed element-wise.

**Definition 42 (Operators on abstract array environments).** For two abstract array environments $a_1$ and $a_2$ on the same typing context $\Gamma$, we define the relation $\sqsubseteq^A$ and the operators $\sqcap^A$, $\sqcup^A$ and $\triangleright^A$ as follows:

$$ a_1 \sqsubseteq^A a_2 \quad \text{iff} \quad \forall x \in \text{Arr}(\Gamma), a_1(x) \sqsubseteq^{\text{Seg}} a_2(x) $$

$$ a_1 \sqcap^A a_2 = [x \mapsto a_1(x) \sqcap^{\text{Seg}} a_2(x)] $$

$$ a_1 \sqcup^A a_2 = [x \mapsto a_1(x) \sqcup^{\text{Seg}} a_2(x)] $$

$$ a_1 \triangleright^A a_2 = [x \mapsto a_1(x) \triangleright^{\text{Seg}} a_2(x)] $$

Since they share the same typing context $\Gamma$, the two abstract array environments $a_1$ and $a_2$ always have the same domain: $\text{Arr}(\Gamma)$. When defining functions, we use the notation

$$ f = [x \mapsto \dots] $$

to mean

$$ \forall x \in \text{dom}(f), f(x) = \dots $$

**Lemma 11 (Soundness of the array domain).** The operations on the array domain are sound:

* $\sqsubseteq^A$ is a pre-order.

* The concretisation $\gamma^A$ is monotonic with respect to the pre-order $\sqsubseteq^A$.

* Abstract union and abstract intersection are sound over-approximations of their concrete counter-parts.

* Widening computes upper bounds and enforces convergence.

### A.1.3 The Tana Product Domain

As explained in Fig. 10, we take a product domain of TanL (N) and A (N). We call this product domain Tana (N), for *Tuple for Algebraic types, Numbers and Arrays*. We do not define a reduction operator for this product domain. When not explicitly defined in this appendix, operators of the product domain are defined component-wise.

### A.1.4 Disjunctive completion

In this appendix, we give the detailed definitions for the Dana domain, which is obtained from the Tana domain by taking a disjunctive completion where cases that
have equivalent constructor constraints are merged together using abstract union. This construction follows the exact same structure than the construction that allows to go from Tan to S (section §3.6.2).

Abstract inclusion is given by a Hoare order:

$$ \mathcal{O}_1 \sqsubseteq^{\mathrm{Tana}} \mathcal{O}_2 \text{ iff } \forall o \in \mathcal{O}_1, \exists o' \in \mathcal{O}_2, o \sqsubseteq^{\mathrm{Tana}} o' $$

Abstract intersection for the disjunctive completion is given by:

$$ \mathcal{O}_1 \sqcap^{\mathrm{Tana}} \mathcal{O}_2 = \mathrm{Collapse}^{\mathrm{Tana}} \left( \left\{ o_1 \sqcap^{\mathrm{Tana}} o_2 \mid \begin{array}{l} o_1 \in \mathcal{O}_1 \wedge o_2 \in \mathcal{O}_2 \wedge \\ o_1 \sqcap^{\mathrm{Tana}} o_2 \neq \bot^{\mathrm{Tana}} \end{array} \right\} \right) $$

We take a disjunction because for certain programs we want to be able to extract information for different cases, in which incompatible constructor names are involved. However, when two abstract values are equivalent with respect to the constructors that they mention, they should be merged, to limit the size of the disjunction. We use the same definition of constructor constraints equivalence as in previous appendix (Definition 16); but this time we extend it for the quadruplets of the Tana domain:

$$ (c_1, e_1, p_1, a_1) \equiv_E^{\mathrm{Tana}} (c_2, e_2, p_2, a_2) \text{ iff } c_1 \equiv c_2 $$

This notion of equivalence allows us to define an operator that collapses together equivalent quadruplets in an element of Dana = $\mathcal{P}(\mathrm{Tana})$.

**Definition 43.** We define an operator $\mathrm{Collapse}^{\mathrm{Tana}}$ that takes a set of elements of Tana and merges together (by taking the abstract union), the elements that are equivalent with respect to $\equiv_E^{\mathrm{Tana}}$. Formally,

$$ \mathrm{Collapse}^{\mathrm{Tana}}(\mathcal{O}) = \left\{ \bigcup_{o \in \bar{o}}^{\mathrm{Tana}} o \mid \bar{o} \in \mathcal{O} / \equiv_E^{\mathrm{Tana}} \right\} $$

We use this collapse operator to provide an abstract union for the Dana domain:

$$ \mathcal{O}_1 \sqcup^{\mathrm{Tana}} \mathcal{O}_2 = \mathrm{Collapse}^{\mathrm{Tana}}(\mathcal{O}_1 \cup \mathcal{O}_2) $$

A widening for the Dana domain is given by

$$ \mathcal{O}_1 \triangleright^{\mathrm{Tana}} \mathcal{O}_2 = \{ o_1 \triangleright^{\mathrm{Tana}} o_2 \mid \begin{array}{l} o_1 \in \mathcal{O}_1 \wedge o_2 \in \mathcal{O}_2 \wedge o_1 \equiv_E^{\mathrm{Tana}} o_2 \\ \cup \{ o_2 \in \mathcal{O}_2 \mid \nexists o_1 \in \mathcal{O}_1, o_1 \equiv_E^{\mathrm{Tana}} o_2 \} \cup \{ o_1 \in \mathcal{O}_1 \mid \nexists o_2 \in \mathcal{O}_2, o_1 \equiv_E^{\mathrm{Tana}} o_2 \} \end{array} \} $$

## A.2 Analysing arrays: transfer functions

In this appendix, we give the transfer functions for Conditions (appendix §A.2.1) and Assignments (appendix §A.2.2) for the domain of segmentations Seg and the domains built on top of it.
### A.2.1 Abstraction for conditions

When analysing a condition (whether it comes from a while loop guard or an assertion), there are up to three things that change in segmentations:

* The segment summaries are modified to integrate the new condition. Here, to keep definitions simple, nothing happens if a segment summary becomes $⊥^S$. We could however, when a segment summary becomes $⊥^S$, have a more precise treatment by looking at the emptiness marker of the segment. If a segment that is not allowed to be empty has a $⊥^S$ summary, then the whole segmentation can be turned into $⊥^{Seg}$. If a segment that is allowed to be empty has a $⊥^S$, then the segment is indeed empty in the concrete, and it can be removed, by merging the boundsets to its left and right.

* Two boundsets may be merged, if the condition implies that they are equal. If this contradicts the (lack of) emptiness markers between the two boundsets, then the whole segmentation becomes $⊥^{Seg}$.

* An emptiness marker may become false, if the condition implies that the associated segment is necessarily non-empty.

We are going to formalize each one of those effects separately, before defining abstraction of conditions for segmentations as a whole.

**Definition 44 (Abstraction of conditions for segmentation summaries).** For any condition c, any array variable x and any segmentation s for variable x given by $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}) \in Seg(\mathbb{N})(\Gamma)(x)$, we define

$$ \mathrm{CondSum}(c)(s) = \left( l, v, b_0, \left( \mathrm{Cond}^{\mathrm{SL}}(c)(d_i), b_i, m_i \right)_{i \in \{1, \dots, n\}} \right) $$

Before describing the effect of conditions on boundsets, we define what it means to merge two boundsets together.

**Definition 45 (Boundset Fusion).** For any segmentation $s = (l, v, b_0, \sigma)$, with a sequence of segments $\sigma = (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}$; and any two segment indices $i_1 \in \{1, \dots, n\}$ and $i_2 \in \{1, \dots, n\}$ such that $i_1 \le i_2$, the fusion of all boundsets between indices $i_1$ and $i_2$ of s is the segmentation defined by

$$ \text{FuseBoundSets}(i_1, i_2, s) = \left\{ \begin{array}{ll} \bot^{\text{Seg}} & \text{if } \exists j, i_1 < j \le i_2, m_j = \mathsf{ff} \\ (l, v, \bigcup_{i_1 \le j \le i_2} b_j, \sigma[i_2 + 1 : n]) & \text{if } i_1 = 0 \text{ and} \\ (l, v, b_0, \sigma[1 : i_1 - 1] \cdot (d_{i_1}, \bigcup_{i_1 \le j \le i_2} b_j, m_{i_1}) \cdot \sigma[i_2 + 1 : n]) & \text{otherwise} \end{array} \right. $$

Merging boundsets assumes that they are equal in the concrete. If any of the emptiness markers between the boundsets being merged is false, this is a contradiction and yields the bottom segmentation.

In the following definitions, we assume that conditions do not include conjunctions or disjunctions. Conjunctions and disjunctions are treated generically, by using abstract intersection (resp. abstract union) on the result of analysing the sub-formulas separately.
Similarly, we assume that the conditions has been pre-treated by applying De Morgan's laws to eliminate negation as much as possible.

**Definition 46** (Abstraction of conditions for segmentation boundsets). For any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1,...,n\})}$ and any condition c, we define

$$ \text{CondBsets}(c)(s) = \left\{ \begin{array}{ll} \text{FuseBoundSets}(i_1, i_2, s) & \begin{array}{l} \text{if } \exists i_1 \in \{0, \dots, n\}, \exists i_2 \in \{0, \dots, n\}, \\ \phantom{\text{if }} \exists e_1 \in b_{i_1}, \exists e_2 \in b_{i_2}, \\ \phantom{\text{if }} c = (e_1 = e_2) \lor (i_1 \le i_2 \land c = (e_1 \ge e_2)) \end{array} \\ \bot^{\text{Seg}} & \begin{array}{l} \text{if } \exists i_1 \in \{0, \dots, n\}, \exists i_2 \in \{0, \dots, n\}, \\ \phantom{\text{if }} \exists e_1 \in b_{i_1}, \exists e_2 \in b_{i_2}, \\ \phantom{\text{if }} i_1 \le i_2 \land c = (e_1 > e_2) \end{array} \\ s & \text{otherwise} \end{array} \right. $$

**Definition 47** (Abstraction of conditions for emptiness markers). For any condition c and any segmentation $s = (l, v, b_0, \sigma)$ with a segment sequence $\sigma = (d_i, b_i, m_i)_{i \in \{1,...,n\}}$, we define

$$ \text{CondMark}(c)(s) = \left\{ \begin{array}{ll} (l, v, b_0, \sigma[1 : i_1 - 1] \cdot (d_{i_1}, b_{i_1}, \mathfrak{f}) \cdot \sigma[i_1 + 1; n]) & \begin{array}{l} \text{if } \exists i_1 \in \{1, \dots, n\}, \\ \phantom{\text{if }} \exists e_1 \in b_{i_1-1}, \exists e_2 \in b_{i_1}, \\ \phantom{\text{if }} c = (e_1 < e_2) \end{array} \\ s & \text{otherwise} \end{array} \right. $$

These three auxiliary definitions allow us to define the abstraction of conditions for segmentations

**Definition 48** (Abstraction of conditions for segmentation). For any condition c and any segmentation s, we define the abstraction of condition c for segmentation s by

$$ \text{Cond}^{\text{Seg}}(c)(s) = (\text{CondSum}(c) \circ \text{CondMark}(c) \circ \text{CondBsets}(c))(s) $$

The order of composition does not affect the final result. It can, however, impact the execution time. We have chosen this order since CondBsets can reduce the number of segments, and both CondMark and CondSum do a traversal of all segments.

This definition is lifted to the A, Tana, Dana and Diorana domains in the standard way. That is, respectively, element-wise, component-wise, disjunct-wise before collapsing
and by priming the condition:

$$ \mathrm{Cond}^{\mathrm{A}}(c)(a) = [x \mapsto \mathrm{Cond}^{\mathrm{Seg}}(c)(a(x))] $$

$$ \mathrm{Cond}^{\mathrm{Tana}}(c)(t, a) = (\mathrm{Cond}^{\mathrm{TanL}}(c)(t), \mathrm{Cond}^{\mathrm{A}}(c)(a)) $$

$$ \mathrm{Cond}^{\mathrm{Dana}}(c)(\mathcal{O}) = \mathrm{Collapse}^{\mathrm{Dana}}\left(\left\{\mathrm{Cond}^{\mathrm{Tana}}(c)(o) \mid o \in \mathcal{O}\right\}\right) $$

$$ \mathrm{Cond}^{\mathrm{Diorana}}(c)(r) = \mathrm{Cond}^{\mathrm{Dana}}(c')(r) $$

### A.2.2 Abstraction for assignments

Abstraction for an assignment $y := e$ behaves differently according to whether a variable of array type is involved (either because $y$ is of array type or because a variable in $e$ has an array type) or not.

#### Abstraction for non-array assignments

Here we look at the assignments of the form $y := e$ where $y$ is not an array variable and no variable appearing in $e$ is an array variable. This means that $e$ is not an array access expression.

We start by formalizing variable replacement inside a bound expression.

**Definition 49** (Variable replacement for bound expressions, boundsets and segmentations). For any variable $y$ and any two bound expressions $e_1$ and $e_2$, the replacement of variable $y$ by bound expression $e_1$ inside bound expression $e_2$ is given by

$$ \mathrm{Replace}^{\mathrm{E}}(y, e_1, e_2) = \begin{cases} x + (k_1 + k_2) & \text{if } e_1 = x + k_1 \text{ and } e_2 = y + k_2 \\ k_1 + k_2 & \text{if } e_1 = k_1 \text{ and } e_2 = y + k_2 \\ e_2 & \text{otherwise} \end{cases} $$

This definition is first extended to boundsets. For any boundset $b$, we define

$$ \mathrm{Replace}^{\mathrm{B}}(y, e_1, b) = \{\mathrm{Replace}^{\mathrm{E}}(y, e_1, e_2) \mid e_2 \in b\} $$

Then, the definition is extended to segmentations in a point-wise manner. Formally, for any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}})$, we define

$$ \mathrm{Replace}^{\mathrm{Seg}}(y, e_1, s) = (l, v, \mathrm{Replace}^{\mathrm{B}}(y, e_1, b_0), (d_i, \mathrm{Replace}^{\mathrm{B}}(y, e_1, b_i), m_i)_{i \in \{1, \dots, n\}}) $$

**Definition 50** (Conditional addition of a bound expression to a boundset). For any variable $y$, any bound expression $e$ and any boundset $b$, we define the addition of $y$ to $b$
conditionally to the presence of e as being the boundset

$$ \text{AddBexp}^{\text{B}}(y, e, b) = \begin{cases} b \cup \{y\} & \text{if } e \in b \\ b & \text{otherwise} \end{cases} $$

We extend this definition to segmentations in a point-wise manner. Formally, for any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, ..., n\}})$ we define

$$ \text{AddBexp}^{\text{Seg}}(y, e, s) = (l, v, \text{AddBexp}^{\text{B}}(y, e, b_0), (d_i, \text{AddBexp}^{\text{B}}(y, e, b_i), m_i)_{i \in \{1, ..., n\}}) $$

This allows us to formalize the effect of assignment on the boundsets of an entire segmentation.

**Definition 51** (Abstraction of non-array assignments for segmentation boundsets). For any segmentation $s$ and any non-array assignment $y := e$, we define

$$ \text{AssignBsets}(y := e)(s) = \begin{cases} \text{Replace}^{\text{Seg}}(y, y - k, s) & \text{if } \exists k \in K, e = y + k \\ \text{AddBexp}^{\text{Seg}}(y, e, \text{RemoveBexp}((y + k | k \in K), s)) & \text{otherwise} \end{cases} $$

For summaries, assignment is propagated to each segment.

**Definition 52** (Abstraction of non-array assignments for segmentation summaries). For any segmentation $s = (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, ..., n\}})$ and any non-array assignment $y := e$, we define

$$ \text{AssignSum}(y := e)(s) = (l, v, b_0, (\text{Assign}^{\text{S}}(y := e)(d_i), b_i, m_i)) $$

The two previous definitions allow us to define what happens to all segmentations when analysing a non-array assignment.

**Definition 53** (Abstraction of non-array assignments for segmentations). For any segmentation $s$ and any non-array assignment $y := e$ the abstraction of assignment $y := e$ for segmentation $s$ is given by

$$ \text{Assign}^{\text{Seg}}(y := e)(s) = (\text{AssignSum}(y := e) \circ \text{AssignBsets}(y := e))(s) $$

When analysing assignments where no variable has an array type (that is, $y$ is not an array variable, and none of the variables appearing in $e$ are either), the transfer function Assign<sup>Seg</sup> can be lifted to the A, Tana, Dana and Diorana domains in the standard way. That is, respectively, element-wise, component-wise, disjunct-wise before
collapsing and by priming all the variables:

$$ Assign^A(y := e)(a) = [x \mapsto Assign^{\text{Seg}}(y := e)(a(x))] $$

$$ Assign^{\text{Tana}}(y := e)(t, a) = (Assign^{\text{TanL}}(c)(t), Assign^A(y := e)(a)) $$

$$ Assign^{\text{Dana}}(y := e)(\mathcal{O}) = \text{Collapse}^{\text{Dana}}(\{Assign^{\text{Tana}}(y := e)(o) | o \in \mathcal{O}\}) $$

$$ Assign^{\text{Diorana}}(c)(r) = Assign^{\text{Dana}}(y' := e')(r) $$

Remember that this kind of assignments can change the segmentations inside the array domain. Indeed, the segment summaries change, and (if $y$ is a numeric variable) the boundsets might also change (Definition 51).

## Abstraction for Array Creation

Here, we look at the assignments of the form $y := \text{new\_array}(\tau^{\text{alg}}, e_1, e_2)$; where $y$ is necessarily an array variable.

**Definition 54** (Transfer Function for Array Creation [Complete Version]). For any algebraic type $\tau^{\text{alg}} \in \text{AlgTypes}$, for any variable $y$ of type Array($\tau^{\text{alg}}$), for any numeric expression $e_1$, any expression $e_2$ of type $\tau^{\text{alg}}$ and any abstract value $(t, a) \in \text{Tana}$, the transfer function for array creation is defined by

$$ \begin{array}{l} \text{Assign}^{\text{Tana}}(y := \text{new\_array}(\tau^{\text{alg}}, e_1, e_2))(t, a) = \\ \quad \begin{cases} \perp^{\text{Tana}} & \text{if Satisfies}^{\text{TanL}}(t, e_1 < 0) \\ (\text{Cond}^{\text{TanL}}(e_1 \ge 0)(t'), a'[y \mapsto s']) & \text{otherwise} \end{cases} \\ \\ \text{where } t' = \begin{cases} \text{Cond}^{\text{TanL}}(|y| = 0)(t) & \text{if Satisfies}^{\text{TanL}}(t, e_1 \le 0) \\ \text{Cond}^{\text{TanL}}(|y| = e_1)(t) & \text{otherwise} \end{cases} \\ \\ \text{and } a' = \text{Assign}^A(|y| := e_1)(a) \\ \\ \text{and } s' = \begin{cases} \{0; |y|\} & \text{if Satisfies}^{\text{TanL}}(t, e_1 \le 0) \\ \{0\} d \{|y|\} & \text{if Satisfies}^{\text{TanL}}(t, e_1 > 0) \\ \{0\} d \{|y|\} & \text{otherwise} \end{cases} \\ \\ \text{and } d = \{\text{Cond}^{\text{TanL}}(0 \le l < e_1 \land v = e_2) (\text{Add}^{\text{TanL}}_{\{l,v\}}(t))\} \end{array} $$

As stated after Definition 35, we distinguish four cases:

* The case where $e_1$ is known to be negative (that is Satisfies$^{\text{TanL}}(t, e_1 < 0)$) and the result is $\perp^{\text{Tana}}$, since any code after this array creation assignment is unreachable.

* The case where $e_1$ is known to be non-positive (that is Satisfies$^{\text{TanL}}(t, e_1 \le 0)$), in which case the new array is known to have size 0, which corresponds with to a segmentation with no segments and a single boundset that contains both zero and the length of the array : $\{0; |y|\}$.

* The case where $e_1$ is known to be positive (that is Satisfies$^{\text{TanL}}(t, e_1 > 0)$). In this case, the emptiness marker of the segmentation is false (as indicated by the absence of a question mark), because we know for certain that the array is not empty.

* All the other cases, where we have no particular prior knowledge on $e_1$, and the result is as described in Definition 35.
Abstraction for array update

In order to define the transfer functions for array update and array access, we start
by describing, for a segmentation, the creation of a new segment at a given bound
expression. We will use this when the index used to access or update an array is a
bound expression.

**Definition 55** (Insert a segment at a bound expression). *Given a segmentation s = (l, v, b₀, σ), with segment sequence σ = (dᵢ, bᵢ, mᵢ)ᵢ∈{1,...,n}, a bound expression e ∈ E(Γ), a segment summary d ∈ S and an abstract value o ∈ Tana, the insertion of segment d at bound expression e in segmentation s, given information o is given by*

$$
\begin{align*}
\text{Insert}^{\text{Seg}}(d, e, s, o) &= (l, v, b'_0, \sigma[1:i_1-1] \cdot \sigma' \cdot \sigma[i_2+1:n]) \\
\text{where} \quad &i_1 = \max\{i \in \{0, \dots, n\} \mid \exists e_1 \in b_i, \text{Satisfies}^{\text{Tana}}(o, e_1 \le e)\} \\
\text{and} \quad &i_2 = \min\{i \in \{0, \dots, n\} \mid \exists e_2 \in b_i, \text{Satisfies}^{\text{Tana}}(o, e < e_2)\} \\
\text{and} \quad &\sigma' = \begin{cases} \sigma_1 \cdot \sigma_e \cdot \sigma_2 & \text{if } i_1 = 0 \\ (d_{i_1}, b'_{i_1}, m_{i_1}) \cdot \sigma_1 \cdot \sigma_e \cdot \sigma_2 & \text{otherwise} \end{cases} \\
\text{and} \quad &b'_{i_1} = \begin{cases} b_{i_1} \cup \{e\} & \text{if } \exists e_1 \in b_{i_1}, \text{Satisfies}^{\text{Tana}}(o, e_1 = e) \\ b_{i_1} & \text{otherwise} \end{cases} \\
\text{and} \quad &b'_0 = \begin{cases} b'_{i_1} & \text{if } i_1 = 0 \\ b_0 & \text{otherwise} \end{cases} \\
\text{and} \quad &\sigma_1 = \begin{cases} \varepsilon & \text{if } \exists e_1 \in b_{i_1}, \text{Satisfies}^{\text{Tana}}(o, e_1 = e) \\ (d', \{e\}, m_L) & \text{otherwise} \end{cases} \\
\text{and} \quad &\sigma_e = (d, b_e, \mathfrak{f}) \\
\text{and} \quad &b_e = \begin{cases} b_{i_2} \cup \{e+1\} & \text{if } \exists e_2 \in b_{i_2}, \text{Satisfies}^{\text{Tana}}(o, e_2 = e+1) \\ \{e+1\} & \text{otherwise} \end{cases} \\
\text{and} \quad &\sigma_2 = \begin{cases} \varepsilon & \text{if } \exists e_2 \in b_{i_2}, \text{Satisfies}^{\text{Tana}}(o, e_2 = e+1) \\ (d', b_{i_2}, m_R) & \text{otherwise} \end{cases} \\
\text{and} \quad &m_L = \exists e_1 \in b_{i_1}, \text{CanSat}^{\text{Tana}}(o, e_1 = e) \\
\text{and} \quad &m_R = \exists e_2 \in b_{i_2}, \text{CanSat}^{\text{Tana}}(o, e_2 = e+1) \\
\text{and} \quad &d' = \bigsqcup_{i_1<i\le i_2}^{\text{SL}} d_i
\end{align*}
$$

Note that for arbitrary abstract values *o*, the segment indices *i*₁ and *i*₂ of Definition 55 might not exist. However, we will always use Insert<sup>Seg</sup> in contexts where *b*₀ contains 0, *b*ₙ contains some length variable |*x*| and *o* contains the information that 0 ≤ *e* < |*x*|, which guarantees the existence of *i*₁ and *i*₂.

For array updates, we distinguish two cases, like [12], depending on whether the
expression used as index can be put in the form of a bound expression or not.

**Definition 56** (Array update at a bound expression). *For any abstract value (t, a), and any bound expression e₁ ∈ E(Γ), the transfer function for the array update instruction*
$y := x[e_1 \to e_2]$ is given by

$$
\begin{align*}
\text{Assign}^{\text{Tana}}(y := x[e_1 \to e_2])(t, a) &= (t_2, a_3) \\
\text{where } (t_2, a_3) &= \text{Assign}^{\text{Tana}}(|y| := |x|)(t_1, a_2) \\
\text{and } a_2 &= a_1[y \mapsto s'] \\
\text{and } s' &= \text{Insert}^{\text{Seg}}(d, e_1, a_1(x), (t_1, a_1)) \\
\text{and } d &= \left\{ \text{Cond}^{\text{TanL}}(l = e_1 \wedge v = e_2) \left( \text{Add}^{\text{TanL}}_{\{l,v\}}(t_1) \right) \right\} \\
\text{and } (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}) &= a_1(x) \\
\text{and } (t_1, a_1) &= \text{Cond}^{\text{Tana}}(0 \le e_1 < |x|)(t, a)
\end{align*}
$$

We are going to explain the formula of array update at a bound expression (Definition 56) from bottom to top. Since expression $e_1$ is used as an index in the array $x$, it must evaluate to an integer between the bounds of the array. Hence we can add the constraint $0 \le e_1 < |x|$ to the information we already have, which is done by the last line: $(t_1, a_1) = \text{Cond}^{\text{Tana}}(0 \le e_1 < |x|)(t, a)$. Then, we get the names for the special index variable $l$ and value variable $v$ by looking at the current segmentation for $x$, which is done in the second-to-last line: $(l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}) = a_1(x)$. We use these special variables $l$ and $v$ to build the segment summary for index $e_1$ for the new array: $d = \{ \text{Cond}^{\text{TanL}}(l = e_1 \wedge v = e_2) \left( \text{Add}^{\text{TanL}}_{\{l,v\}}(t_1) \right) \}$. This allows to define the segmentation $s'$ for the new array, by inserting the segment summary $d$ at index $e_1$ (which is possible since $e_1$ is a bound expression): $s' = \text{Insert}^{\text{Seg}}(d, e_1, a_1(x), (t_1, a_1))$. The new array environment is obtained by associating this new segmentation $s'$ to the variable $y$ being assigned: $a_2 = a_1[y \mapsto s']$. The length of the array now stored in $y$ is the same as the array stored in $x$, and this must be taken into account both inside numeric constraints but also in boundsets. This information is updated by $(t_2, a_3) = \text{Assign}^{\text{Tana}}(|y| := |x|)(t_1, a_2)$, which yields our final result.

**Definition 57 (Array update at a non-bound expression).** For any abstract value $(t, a)$, and any expression $e_1$ that is not a bound expression, the transfer function for the array update instruction $y := x[e_1 \to e_2]$ is given by

$$
\begin{align*}
\text{Assign}^{\text{Tana}}(y := x[e_1 \to e_2])(t, a) &= (t_2, a_3) \\
\text{where } (t_2, a_3) &= \text{Assign}^{\text{Tana}}(|y| := |x|)(t_1, a_2) \\
\text{and } a_2 &= a[y \mapsto s'] \\
\text{and } s' &= (l, v, b_0, (d'_i, b_i, m_i)_{i \in \{1, \dots, n\}}) \\
\text{and } \forall i \in I, d'_i &= d_i \sqcup^{\text{SL}} \left\{ \text{Cond}^{\text{TanL}}(l = e_1 \wedge v = e_2) \left( \text{Add}^{\text{TanL}}_{\{l,v\}}(t_1) \right) \right\} \\
\text{and } \forall i \in \{1, \dots, n\} \setminus I, d'_i &= d_i \\
\text{and } I &= \{ i \in [1, n] \mid \exists (e_L, e_R) \in b_{i-1} \times b_i, \text{CanSat}^{\text{Tana}}((t_1, a_1), e_L \le e_1 < e_R) \} \\
\text{and } (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}) &= a_1(x) \\
\text{and } (t_1, a_1) &= \text{Cond}^{\text{Tana}}(0 \le e_1 < |x|)(t, a)
\end{align*}
$$

Definition 57 is very similar to Definition 56. The difference lies in the segment summaries. Since $e_1$ is not a bound expression, it is not possible to create a segment of length exactly one to store in a precise way the information about the new value. Instead, the set $I$ identifies all possible segments that might be indexed by $e_1$, and for
these segments a union between the old value and the new value is taken. Said otherwise, Definition 56 performs a strong update while Definition 57 performs a weak update.

### Abstraction for array accesses

When analysing an array access instruction $y := x[e]$, three different things happen:

* The segmentation for variable $x$ is used to deduce information on the new value of variable $y$.

* If $e$ is a bound expression, a new segment is created inside the segmentation for $x$, of size one, whose only possible index is $e$. For this new segment, we know that its value is equal to the new value of $y$. Hence any information that we learn from $y$ going forward, also enriches the segmentation for $x$.

* If $y$ appears in bound expressions inside the boundsets of segmentations, the corresponding bound expressions are removed.

Let's look at an example of array access. In this example, we will omit the disjunctive completion, constructor constraints and structural equalities, to focus on the NPR and array components. For example, if we analyse the assignment $y := t[x]$ while already having the abstract value

$$ \left( \begin{array}{l} \{5 \le x; |t| = 10\}, \\ [t \mapsto (l, v, \{0\} \quad v \le 0 \quad \{5\} \quad v = l + 1 \quad \{7\} \quad v = 2 \times l \quad \{|t|\})] \end{array} \right) $$

then, the abstract value after the assignment should be

$$ \left( \begin{array}{l} \{5 \le x < 10; 6 \le y \le 18; |t| = 10\}, \\ [t \mapsto (l, v, \{0\} \quad v \le 0 \quad \{5\} \quad v = l + 1 \quad \{7\} \quad v = 2 \times l \quad \{|t|\})] \end{array} \right) $$

where we have gained information both on variable $x$ and on variable $y$. Indeed, $x$ being used as index tells us that $x$ is smaller than $|t|$; while the information for $y$ is obtained from joining what would happen for two different segments: the segment between indices 5 and 7 (5 included and 7 excluded) and the segment between indices 7 and $|t|$ (7 included and $|t|$ excluded). This results in joining the information $\{y = x+1; 5 \le x < 7\}$ with the information $\{y = 2 \times x; 7 \le x < 10\}$ which results in $\{6 \le y \le 18; 5 \le x < 10\}$.

We start by defining the removal of the bound expressions containing $y$. This is similar to what is done for non-array assignments (Definition 51), but simpler, since we only remove, without adding nor replacing.

**Definition 58** (Abstraction of array access for segmentation boundsets). For any segmentation $s$ and any array access assignment $y := x[e]$, we define

$$ \text{AssignBsets}(y := x[e])(s) = \text{RemoveBexp}(\{y + k \mid k \in K\}, s) $$

We then define the effect of array access on abstract array environments: in addition to the removal of $y$ from the boundsets it appears to, the segmentation associated to $x$ is used to deduce information about $y$ that will be added to the segment summaries of the other segmentations.

**Definition 59** (Abstraction of array access for abstract array environments). For any abstract array environment $a$ and any array access assignment $y := x[e]$, the
abstraction of array access $y := x[e]$ for abstract array environment *a* is the abstract array environment such that, for any array variable *z*,

$$
\begin{align*}
\text{Assign}^A(y := x[e])(a, t)(z) &= \\
&\quad \left( l, v, b_0^z, (d_i^z, b_i^z, m_i^z)_{i \in \{1, \dots, p\}} \right) \\
\text{where} \quad \forall i \in \{1, \dots, p\}, \quad &d_i^{z'} = d_e \sqcap^{\text{SL}} \text{Add}_{\{y\}}^{\text{SL}} (\text{Rem}_{\{y\}}^{\text{SL}}(d_i^z))
\end{align*}
$$

$$
\text{and} \quad d_e = \bigsqcup_{i=i_1+1}^{i_2} \text{Assign}^{\text{SL}}(y := v) \left( \text{Cond}^{\text{SL}}(l=e)(d_i^x) \right)
$$

$$
\text{and} \quad i_1 = \max \{ i \in \{0, \dots, n\} \mid \exists e_1 \in b_i^x, \text{Satisfies}^{\text{Tana}}((t, a), e_1 \le e) \}
$$

$$
\text{and } i_2 = \min \{ i \in \{0, \dots, n\} \mid \exists e_2 \in b_i^x, \text{Satisfies}^{\text{Tana}}((t, a), e < e_2) \}
$$

$$
\text{and} \quad (l, v, b_0^x, (d_i^x, b_i^x, m_i^x)_{i \in \{1, \dots, n\}}) = a(x)
$$

$$
\text{and} \quad (l, v, b_0^z, (d_i^z, b_i^z, m_i^z)_{i \in \{1, \dots, p\}}) = \text{AssignBsets}(y := x[e])(a(z))
$$

In the detailed example of appendix §B, the fact of creating a new segment at array access proves very useful. Indeed, it allows, after assignment `challenger = q[i]`, to take into account inside the segmentation the assertions made on variable `challenger`, like, for example, the assertion `assert(res@SomeMax.prio >= challenger.prio)` on the third branch. The knowledge of how the array content relates to the value of variable `res` is what allows to capture into the function summary the information that the result has a priority higher to any of the TCBs in the queue.

Because of this creation of a new segment, array access definition is similar to the
one for array update. In particular, there are two cases according to whether the index
being accessed is a bound expression or not.

**Definition 60 (Abstraction of array access at a bound expression).** For any abstract value $(t, a) \in \text{Tana}$ and any array access instruction $y := x[e]$ where $e$ is a bound expression, the abstraction for array access is given by

$$
\begin{align*}
\text{Assign}^{\text{Tana}}(y := x[e])(t, a) &= (t', a') \\
\text{where} \quad a' &= \text{Assign}^{A}(y := x[e])(a'', t')
\end{align*}
$$

$$
\text{and} \quad a'' = a[y \mapsto s']
$$

$$
\text{and} \quad s' = \text{Insert}^{\text{Seg}}(d, e, a(x), (t', a))
$$

$$
\text{and} \quad t' = \text{Rem}_{\{l,v\}}^{\text{TanL}} \left( \bigsqcup_{t'' \in d}^{i_2} t'' \right)
$$

$$
\text{and} \quad d = \bigsqcup_{i=i_1+1}^{i_2} \text{Assign}^{\text{SL}}(y := v) \left( \text{Cond}^{\text{SL}}(l=e \land 0 \le e < |x|)(d_i) \right)
$$

$$
\text{and} \quad i_1 = \max \{ i \in \{0, \dots, n\} \mid \exists e_1 \in b_i, \text{Satisfies}^{\text{Tana}}((t, a), e_1 \le e) \}
$$

$$
\text{and } i_2 = \min \{ i \in \{0, \dots, n\} \mid \exists e_2 \in b_i, \text{Satisfies}^{\text{Tana}}((t, a), e < e_2) \}
$$

$$
\text{and} \quad (l, v, b_0, (d_i, b_i, m_i)_{i \in \{1, \dots, n\}}) = a(x)
$$

The abstraction of array access at a non-bound expression is given in Definition 36, Page 47, on the main text of the article.
## B Detailed example of analysis with arrays

In this appendix, we manually execute the analysis on the find_max_priority function from Fig. 8. To alleviate notation, we use the following conventions in the description that follows:

* If a set of abstract values in a disjunctive completion is a singleton, then we omit the braces. For example, in a structural equalities component, we write $q' = q$ instead of $\{q' = q\}$.

* If a constraint can be deduced from other constraints already written, it can be omitted. For example, if we have a structural equalities component $q' = q$ and the NPR component can be described by the set of constraints $\{|q| > 0; |q'| > 0\}$, then one of the two constraints of the NPR component can be omitted, and we write $|q'| > 0$.

* We may omit an entire component of a product domain when the component is $\top$, or when all its constraints can be deduced from other components.

* We use labels to better identify components of an abstract value: we use the label `cc` for the constructor constraints component, `seq` for the structural equalities component, `NPR` for the NPR component, `A` for the array component.

We start the analysis of the function with the identity relation between the primed and un-primed versions of the arguments, together with the top segmentation for arrays. The top segmentation for arrays implies that every array length is non-negative. Hence, the initial abstract value is

$$r_0 = \left( \begin{array}{ll} \mathbf{seq} : q' = q, & \mathbf{NPR} : |q'| \ge 0 \\ \mathbf{A} : [q' \mapsto \{0\} \supset \{|q'|\}|?] & \end{array} \right)$$

After the first two assignments $i = 0; \text{res} = \text{NoMax} \{\}$, we get the abstract value

$$r_1 = \left( \begin{array}{ll} \mathbf{cc} : \text{res}'@\text{NoMax}, & \mathbf{seq} : q' = q, \\ \mathbf{A} : [q' \mapsto \{0; i'\} \supset \{|q'|\}|?] & \end{array} \right)$$

We see that, in addition to gaining the constructor constraint $\text{res}'@\text{NoMax}$, the bound expression $i'$ was added to the set of bound expressions that contained 0, since, after the assignment, we have $i' = 0$. The variable $i'$ is added by the first boundset thanks to the AddBexp$^B$ function, that is used by the transfer function for assignments. This is formalised in Definitions 42, 50, 51 and 53.

When analysing the loop, we use loop unrolling. Hence, the results of not executing the loop at all, and executing it at least once, are computed separately, and then joined afterwards. The result of not executing the loop at all is obtained by applying the transfer function for condition $i' \ge |q'|$ to the abstract value before the loop, and produces the following abstract value:

$$r_2 = \text{Cond}^{\text{Dana}}(i' \ge |q'|)(r_1) = \left( \begin{array}{ll} \mathbf{cc} : \text{res}'@\text{NoMax}, & \mathbf{seq} : q' = q, \\ \mathbf{A} : [q' \mapsto \{0; i'; |q'|\}] & \end{array} \right)$$
In the NPR component, the new condition $i' \ge |q'|$ combined with the information that we already had $i' \le |q'|$ allows to deduce $i' = |q'|$. In the array component, in the segmentation for $q'$, the two former boundsets $\{0; i'\}$ and $\{|q'|\}$ are merged by the FuseBoundSets function. Indeed, there is no segment between $i'$ and $|q'|$, since $i' = |q'|$. This is formalized in Definitions 45, 46 and 48. We get for $q'$ a segmentation with only one set of segment bounds and no segment summary; in other words, a segmentation for the empty array.

To obtain the result of executing the loop at least once, we start by analysing one execution of the loop body, then we look for a fixpoint with a Kleene iteration with widening. When entering the loop the first time, we get

$$r_3 = \text{Cond}^{\text{Dana}}(i' < |q'|)(r_1) = \left( \begin{array}{l} \textbf{cc} : \text{res}'@\text{NoMax}, \quad \textbf{seq} : q' = q, \quad \textbf{NPR} : \{|q'| > 0; i' = 0\} \\ \textbf{A} : [q' \mapsto \{0; i'\} \uplus \{|q'|\}] \end{array} \right)$$

The condition tells us that the segment between $\{0; i'\}$ and $\{|q'|\}$ is not empty, since $i' < |q'|$. Hence the question mark indicating that the segment can be empty disappears from the array segmentation. This is formalized in Definition 47.

Then, analysing the assignment `challenger = q[i]` creates a new segment, between bound expressions $i$ and $i + 1$, for the segmentation of $q'$.

$$r_4 = \text{Assign}^{\text{Dana}}(\text{challenger}' := q'[i])(r_3) = \left( \begin{array}{l} \textbf{cc} : \text{res}'@\text{NoMax}, \quad \textbf{seq} : q' = q, \quad \textbf{NPR} : \{|q'| > 0; i' = 0\} \\ \textbf{A} : [q' \mapsto \{0; i'\} \left( \textbf{NPR} : \left\{ \begin{array}{l} l = i' = 0; \\ v = \text{challenger}' \end{array} \right\} \right) \{i' + 1\} \uplus \{|q'|\}] \end{array} \right)$$

The insertion of this segment of size 1 is performed by the `Insert<sup>Seg</sup>` function, and is formalized in Definitions 55 and 60.

To analyse the branching, the tree branches are analysed separately, and then the results are joined together. Here, for the first iteration of the loop, only the first branch of the branching is reachable. Indeed, for the second and third branches, the assertions introduce the path `res'@SomeMax.prio`, which is incompatible with the path `res'@NoMax` already present. The analysis therefore infers that the second and third branches are unreachable and produces $\perp$Diorana. Hence, the result of the whole branching construct for this first loop iteration is the result of analysing the first branch. The first assignment of the first branch adds a structural equality to our abstract value:

$$r_5 = \text{Assign}^{\text{Dana}}(\text{case}' := \text{res}'@\text{NoMax})(r_4) = \left( \begin{array}{l} \textbf{cc} : \text{res}'@\text{NoMax}, \quad \textbf{seq} : \left\{ \begin{array}{l} q' = q; \\ \text{case}' = \text{res}'@\text{NoMax} \end{array} \right\}, \quad \textbf{NPR} : \left\{ \begin{array}{l} |q'| > 0; \\ i' = 0 \end{array} \right\} \\ \textbf{A} : [q' \mapsto \{0; i'\} \left( \textbf{NPR} : \left\{ \begin{array}{l} l = i' = 0; \\ v = \text{challenger}' \end{array} \right\} \right) \{i' + 1\} \uplus \{|q'|\}] \end{array} \right)$$

The second assignment of the first branch changes the constructor constraint on `res'`, and allows us to gain some information for the array segment contained between the
bounds $i'$ and $i' + 1$:

$$r_6 = \text{Assign}^{\text{Dana}}(\text{res}' := \text{SomeMax}(\text{challenger}'))(r_5) = \\ \left( \begin{array}{c} \text{seq} : \{\text{res}'@\text{SomeMax} = \text{challenger}'; q' = q\}, \quad \text{NPR} : \{|q'| > 0; i' = 0\} \\ \text{A} : \left[ q' \mapsto \{0; i'\} \quad \text{NPR} : \left\{ \begin{array}{l} l = i' = 0; \\ v = \text{challenger}' \\ v = \text{res}'@\text{SomeMax} \end{array} \right\} \{i' + 1\} \supset \{|q'|\} \right] \end{array} \right)$$

After the branching, the next instruction is the assignment $i := i + 1$. This assignment is invertible, in the sense that the value of variable $i$ after the assignment is an expression on the value of $i$ before the assignment. The inverse of this assignment is $i := i - 1$. The expression $i - 1$ in this inverse assignment can be used as a segment bound. Hence we update the bound segments by replacing $i'$ with $i' - 1$ (in addition to updating the NPR components and the segment summaries). This is obtained thanks to the function Replace<sup>Seg</sup> and formalized in Definitions 49 and 51. We get

$$r_7 = \text{Assign}^{\text{Dana}}(i' := i' + 1)(r_6) = \\ \left( \begin{array}{c} \text{seq} : \{\text{res}'@\text{SomeMax} = \text{challenger}'; q' = q\}, \quad \text{NPR} : \{|q'| > 0; i' = 1\}, \\ \text{A} : \left[ q' \mapsto \{0; i' - 1\} \quad \text{NPR} : \left\{ \begin{array}{l} l = i' - 1 = 0; \\ v = \text{challenger}' \\ v = \text{res}'@\text{SomeMax} \end{array} \right\} \{i'\} \supset \{|q'|\} \right] \end{array} \right)$$

This abstract value $r_7$, that corresponds to the end of the first abstract execution of the loop, will not only be used to compute the second abstract execution of the loop, but also to take a widening with the result of that second execution.

The second abstract execution of the loop body starts with the loop condition

$$r_8 = \text{Cond}^{\text{Dana}}(i' < q')(r_7) = \\ \left( \begin{array}{c} \text{seq} : \{\text{res}'@\text{SomeMax} = \text{challenger}'; q' = q\}, \quad \text{NPR} : \{|q'| > 1; i' = 1\} \\ \text{A} : \left[ q' \mapsto \{0; i' - 1\} \quad \text{NPR} : \left\{ \begin{array}{l} l = i' - 1 = 0; \\ v = \text{challenger}' \\ v = \text{res}'@\text{SomeMax} \end{array} \right\} \{i'\} \supset \{|q'|\} \right] \end{array} \right)$$

As before, the loop condition allows to establish that the last segment of the segmentation is not empty.

Then we have to analyse the assignment to variable `challenger`, and we obtain

$$r_9 = \text{Assign}^{\text{Dana}}(\text{challenger}' := q'[i']) (r_8) = \\ \left( \begin{array}{c} \text{cc} : \text{res}'@\text{SomeMax}, \quad \text{seq} : q' = q, \quad \text{NPR} : \{|q'| > 1; i' = 1\} \\ \text{A} : \left[ q' \mapsto \{0; i' - 1\} d_1^9 \{i'\} d_2^9 \{i' + 1\} \supset \{|q'|\} \right] \end{array} \right) \\ \text{where } d_1^9 = \left( \text{NPR} : \left\{ \begin{array}{l} l = i' - 1 = 0; \\ v = \text{res}'@\text{SomeMax} \end{array} \right\} \right) \\ \text{and } d_2^9 = \left( \text{NPR} : \left\{ \begin{array}{l} l = i' = 1; \\ v = \text{challenger} \end{array} \right\} \right)$$
As before, this assignment creates a new segment in the segmentation, between bounds $i'$ and $i' + 1$.

During this second abstract execution of the loop, the first branch of the branching is unreachable and its analysis yields $\perp^{\text{Diorana}}$, while the other two branches are reachable. The assertion on the second branch yields

$$ 
\begin{align*}
r_{10} = \text{Cond}^{\text{Dana}}(\text{challenger}^{\prime}\text{.prio} > \text{res}^{\prime}\text{@SomeMax.prio})(r_9) &= \\
&\quad \left( \begin{array}{@{}l@{}}
    \mathbf{cc} : \text{res}^{\prime}\text{@SomeMax}, \mathbf{seq} : q' = q, \\
    \mathbf{NPR} : \{ |q'| > 1; i' = 1; \text{challenger}^{\prime}\text{.prio} > \text{res}^{\prime}\text{@SomeMax.prio}\} \\
    \mathbf{A} : [q' \mapsto \{0; i' - 1\} d_1^{10} \{i'\} d_2^{10} \{i' + 1\} \top \{ |q'| \} ?]
  \end{array} \right) \\
\text{where } d_1^{10} &= \left( \text{NPR} : \left\{ \begin{array}{@{}l@{}}
    l = i' - 1 = 0; v = \text{res}^{\prime}\text{@SomeMax} \\
    v.\text{prio} < \text{challenger}^{\prime}\text{.prio}
  \end{array} \right\} \right) \\
\text{and } d_2^{10} &= \left( \text{NPR} : \left\{ \begin{array}{@{}l@{}}
    l = i' = 1; \\
    v = \text{challenger}^{\prime}
  \end{array} \right\} \right)
\end{align*}
$$

We see that the fact that the segment summaries mention variables of the program other than $l$ and $v$ (like $\text{res}'$ and $\text{challenger}'$ here) allows to capture interesting information on the array contents. For example, here, the inequality $v.\text{prio} < \text{challenger}'\text{.prio}$ inside the first segment summary $d_1^{10}$, that will allow, as the analysis continues, to deduce that the priorities of all TCBs in the array are less than or equal to the one of the final result.

Then, after the assignment of the second branch, we have

$$ 
\begin{align*}
r_{11} = \text{Assign}^{\text{Dana}}(\text{res}' := \text{SomeMax}(\text{challenger}'))(r_{10}) &= \\
&\quad \left( \begin{array}{@{}l@{}}
    \mathbf{cc} : \text{res}'\text{@SomeMax}, \quad \mathbf{seq} : \{q' = q; \text{res}'\text{@SomeMax} = \text{challenger}'\}, \\
    \mathbf{NPR} : \{ |q'| > 1; i' = 1\} \\
    \mathbf{A} : [q' \mapsto \{0; i' - 1\} d_1^{11} \{i'\} d_2^{11} \{i' + 1\} \top \{ |q'| \} ?]
  \end{array} \right) \\
\text{where } d_1^{11} &= \left( \text{NPR} : \left\{ \begin{array}{@{}l@{}}
    l = i' - 1 = 0; \\
    v.\text{prio} < \text{res}'\text{@SomeMax.prio}
  \end{array} \right\} \right) \\
\text{and } d_2^{11} &= \left( \text{NPR} : \left\{ \begin{array}{@{}l@{}}
    l = i' = 1; \\
    v = \text{challenger}'
  \end{array} \right\} \right)
\end{align*}
$$

If we compare the first segment summary in this abstract value $r_{11}$ with the previous abstract value $r_{10}$, we see that the previous equality $v = \text{res}'\text{@SomeMax}$ has disappeared, since the value of $\text{res}'$ has changed; but a new inequality $v.\text{prio} < \text{res}'\text{@SomeMax.prio}$ has been deduced from the previous inequality $v.\text{prio} < \text{challenger}'\text{.prio}$.

For the third branch, the constraint $\text{res}'\text{@SomeMax.prio} \ge \text{challenger}'\text{.prio}$ is captured by the NPR component of the Tana product. This is the only change with
respect to the abstract value before the branching.

$$
\begin{align*}
r_{12} = \text{Cond}^{\text{Dana}}(\text{res}'@\text{SomeMax.prio} \ge \text{challenger}'\text{.prio})(r_9) = & \\
& \left( \begin{array}{@{}l@{}}
    \text{cc} : \text{res}'@\text{SomeMax}, \quad \text{seq} : q' = q, \\
    \text{NPR} : \{ |q'| > 1; i' = 1; \text{res}'@\text{SomeMax.prio} \ge \text{challenger}'\text{.prio}\} \\
    \text{A} : [ q' \mapsto \{0; i' - 1\} d_1^{12} \{i'\} d_2^{12} \{i' + 1\} \supset \{ |q'| \} ? ]
  \end{array} \right) \\
\text{where } d_1^{12} = & \left( \text{NPR} : \begin{cases} l = i' - 1 = 0; \\ v = \text{res}'@\text{SomeMax} \end{cases} \right) \\
\text{and } d_2^{12} = & \left( \text{NPR} : \begin{cases} l = i' = 1; \\ v = \text{challenger}' \end{cases} \right)
\end{align*}
$$

At the end of the branching, we get the union of the abstract value for the second branch $r_{11}$, and the abstract value for the third branch $r_{12}$ (recall the first branch is unreachable and its abstract value $\perp^{\text{Diorana}}$ at this point).

$$
\begin{align*}
r_{13} = r_{11} \sqcup^{\text{Diorana}} r_{12} = & \\
& \left( \begin{array}{@{}l@{}}
    \text{cc} : \text{res}'@\text{SomeMax}, \quad \text{seq} : q' = q, \\
    \text{NPR} : \{ |q'| > 1; i' = 1; \text{res}'@\text{SomeMax.prio} \ge \text{challenger}'\text{.prio}\} \\
    \text{A} : [ q' \mapsto \{0; i' - 1\} d_1^{13} \{i'\} d_2^{13} \{i' + 1\} \supset \{ |q'| \} ? ]
  \end{array} \right) \\
\text{where } d_1^{13} = & \left( \text{NPR} : \begin{cases} l = i' - 1 = 0; \\ v.prio \le \text{res}'@\text{SomeMax.prio} \end{cases} \right) \\
\text{and } d_2^{13} = & \left( \text{NPR} : \begin{cases} l = i' = 1; \\ v = \text{challenger}' \end{cases} \right)
\end{align*}
$$

One interesting thing to note here, is the value of the first segment summary. Indeed, in the second branch we have $v.prio < res'@SomeMax.prio$ whereas in the third branch we have both $v = res'@SomeMax$ and $res'@SomeMax.prio \ge challenger'.prio$, hence the union of the two yields $v.prio \le res'@SomeMax.prio$. Intuitively, we go from the two cases “A TCB with a higher priority has been found in the array, and stored in variable res” and “The TCB stored in res is still the one with the highest priority so far” to the invariant “Whatever the case, the priority of the TCB stored in res is higher or equal to the ones in the array, between indices 0 included, and i excluded”.

The last instruction of the loop body is the increment of variable *i*. As before, this updates the bound expressions used to delimit segments, in addition to update segment summaries.

$$
\begin{align*}
r_{14} = \text{Assign}^{\text{Dana}}(i' := i' + 1)(r_{13}) = & \\
& \left( \begin{array}{@{}l@{}}
    \text{cc} : \text{res}'@\text{SomeMax}, \quad \text{seq} : q' = q, \\
    \text{NPR} : \{ |q'| > 1; i' = 2; \text{res}'@\text{SomeMax.prio} \ge \text{challenger}'\text{.prio}\} \\
    \text{A} : [ q' \mapsto \{0; i' - 2\} d_1^{14} \{i' - 1\} d_2^{14} \{i'\} \supset \{ |q'| \} ? ]
  \end{array} \right) \\
\text{where } d_1^{14} = & \left( \text{NPR} : \begin{cases} l = i' - 2 = 0; \\ v.prio \le \text{res}'@\text{SomeMax.prio} \end{cases} \right) \\
\text{and } d_2^{14} = & \left( \text{NPR} : \begin{cases} l = i' - 1 = 1; \\ v = \text{challenger}' \end{cases} \right)
\end{align*}
$$
The next step of the analysis is to take a widening between abstract value $r_7$ that was obtained at the end of the first execution of the loop, and abstract value $r_{14}$, obtained at the end of the second execution of the loop. In order to perform the widening, we start by transforming the segmentations that appear in these two abstract values, so that they have the same sets of bound expressions; this is called unification. In this detailed example, when unifying segmentations for widening, we will only use bound expression removal, and not boundset splitting (section §6.5.1). Although less precise in general, it will be precise enough for this example, and allows for faster convergence, which is useful in hand-executed analyses. In this example, not using boundset splitting forces the removal of bound expression $i' - 1$, which means that the two first segments of $r_{14}$ are merged together, using abstract union. After unification we get

$$r'_7 = \left( \begin{array}{l} \mathbf{seq} : \{res'@SomeMax = challenger'; q' = q\}, \quad \mathbf{NPR} : \{|q'| > 0; i' = 1\}, \\ \mathbf{A} : \left[ q' \mapsto \{0\} \quad \mathbf{NPR} : \left\{ \begin{array}{l} l = i' - 1 = 0; \\ v = challenger' \\ v = res'@SomeMax \end{array} \right\} \right] \{i'\} \supset \{|q'|\}? \end{array} \right)$$

and

$$r'_{14} = \left( \begin{array}{l} \mathbf{cc} : res'@SomeMax, \quad \mathbf{seq} : q' = q, \\ \mathbf{NPR} : \{|q'| > 1; i' = 2; res'@SomeMax.prio \ge challenger'.prio\} \\ \mathbf{A} : \left[ q' \mapsto \{0\} \quad \mathbf{NPR} : \left\{ \begin{array}{l} i' - 2 \le l \le i' - 1; i' = 2; \\ v.prio \le res'@SomeMax.prio \end{array} \right\} \right] \{i'\} \supset \{|q'|\}? \end{array} \right)$$

We see that, as intended, the segmentations share the same sets of bound expressions after unification: $\{0\}$, $\{i'\}$ and $\{|q'|\}$. To go from $r_7$ to $r'_7$ the bound expression $i' - 1$ was removed from the boundset $\{0; i' - 1\}$. To go from $r_{14}$ to $r'_{14}$, the bound expressions $i' - 2$ and $i' - 1$ were removed from their respective bound expressions, and the two first segments were merged. Everything else remained unchanged. Both of these transformations yield abstract values that are less precise than the initial ones. In other words, $r_7 \subseteq$Diorana $r'_7$ and $r_{14} \subseteq$Diorana $r'_{14}$. This is the reason why it is sound to perform unification for widening.

After unification, widening is done segment-wise. The result of the widening is

$$r_{15} = \left( \begin{array}{l} \mathbf{cc} : res'@SomeMax, \quad \mathbf{seq} : q' = q, \\ \mathbf{NPR} : \{|q'| > 0; i' \ge 1; res'@SomeMax.prio \ge challenger'.prio\} \\ \mathbf{A} : \left[ q' \mapsto \{0\} \quad \mathbf{NPR} : \left\{ \begin{array}{l} 0 \le l \le i' - 1; i' \ge 1; \\ v.prio \le res'@SomeMax.prio \end{array} \right\} \right] \{i'\} \supset \{|q'|\}? \end{array} \right)$$

We see that during unification and widening, the distinction between the last slot of the array to be treated (the one at $i - 1$) and the others before it has disappeared. Instead we have a single segment for all the slots treated so far (between indices 0 included and $i$ excluded), with the invariant that their TCB's priority is smaller or equal to the one in variable res.
This is a fixpoint. We recall that in the context of loop unrolling, we computed separately the abstract value for the executions where the loop is not taken at all ($r_2$), from the abstract value for all the executions that take the loop at least once. The latter is obtained from fixpoint $r_{15}$ by applying the negation of the loop condition:

$$r_{16} = \text{Cond}^{\text{Dana}}(i' \ge |q'|)(r_{15}) = \left( \begin{array}{l} \texttt{cc} : res'@\text{SomeMax}, \quad \texttt{seq} : q' = q, \\ \texttt{NPR} : \{ |q'| = i'; i' \ge 1; res'@\text{SomeMax.prio} \ge \text{challenger'}.\text{prio} \} \\ \texttt{A} : [ q' \mapsto \{0\} \left( \texttt{NPR} : \left\{ \begin{array}{l} 0 \le l \le i' - 1; i' \ge 1; \\ v.prio \le res'@\text{SomeMax.prio} \end{array} \right) \right) \{i'; |q'|\} ] \end{array} \right)$$

Like before for $r_2$, the condition $i' \ge |q'|$ together with the information already present $i' \le |q'|$ allows to deduce that $i' = |q'|$, and hence allows to merge the two sets of bound expressions $\{i'\}$ and $\{|q'|\}$.

The abstract value after the loop, that accounts for the execution that do not take the loop at all, and those that take it at least once, is

$$r_{17} = r_2 \sqcup^{\text{Diorana}} r_{16} = \left\{ \begin{array}{l} \left( \begin{array}{l} \texttt{cc} : res'@\text{NoMax}, \quad \texttt{seq} : q' = q, \quad \texttt{NPR} : i' = 0 = |q'| \\ \texttt{A} : [ q' \mapsto \{0; i'; |q'| \} ] \end{array} \right); \\ \left( \begin{array}{l} \texttt{cc} : res'@\text{SomeMax}, \quad \texttt{seq} : q' = q, \\ \texttt{NPR} : \{ |q'| = i'; i' \ge 1; res'@\text{SomeMax.prio} \ge \text{challenger'}.\text{prio} \} \\ \texttt{A} : [ q' \mapsto \{0\} \left( \texttt{NPR} : \left\{ \begin{array}{l} 0 \le l \le i' - 1; i' \ge 1; \\ v.prio \le res'@\text{SomeMax.prio} \end{array} \right) \right) \{i'; |q'|\} ] \end{array} \right) \end{array} \right\}$$

Since the two abstract values $r_2$ and $r_{16}$ have incompatible constructor constraints $res'@\text{NoMax}$ and $res'@\text{SomeMax}$; they are both kept in the disjunction, as separate cases.

The input-output summary for the function is then obtained by removing all the variables except the input variable $q$ and the output variable $res'$. The structural equality $q' = q$ allows to transport all the information gathered on $q'$ to $q$. The summary that we get for the `find_max_priority` function is

$$\left\{ \begin{array}{l} ( \texttt{cc} : res'@\text{NoMax}, \quad \texttt{NPR} : |q| = 0, \quad \texttt{A} : [ q \mapsto \{0; |q| \} ] ); \\ ( \texttt{cc} : res'@\text{SomeMax}, \quad \texttt{NPR} : |q| \ge 1, \\ \quad \texttt{A} : [ q \mapsto \{0\} \left( \texttt{NPR} : l \ge 0; v.prio \le res'@\text{SomeMax.prio} \right) \{ |q| \} ] ) \end{array} \right\}$$

As stated in section §6.8, this input-output summary distinguishes two cases:

* either the input queue is empty ($|q| = 0$) and the result is built using constructor `NoMax`;

* or the input queue is not empty ($|q| > 1$), the result is built using constructor `SomeMax` and the TCB that is returned as a result (via the constructor `SomeMax`) has a priority that is greater than the priority of any of the TCBs in the input queue.
As we stated before, this input-output summary is not exact: it does not state that, when the result is a TCB wrapped in constructor SomeMax, this TCB belongs to the input queue.