We define an abstract interpreter for programs manipulating scalars, immutable non-recursive algebraic data types (ADTs), functional arrays and non-recursive functions. We define a first domain that expresses relations between values of ADTs. Our domain extends numeric domains in a generic way, by a disjunctive completion over a reduced product of domains for numeric relations, equalities, and variant constructors. We further extend the segmentation approach for array analysis, in order to allow for values of ADTs inside arrays, and also to capture relations between the content of arrays and the other variables in the program. Our analysis is inter-procedural and modular: it proceeds by computing summaries of the input-output relations of functions, which are then instantiated at call sites. The analysis of ADTs has been implemented in OCaml and tested on a sample of small-to-medium examples, some of which are simplified versions of functions from the formal specification of the seL4 microkernel.
