Lifting Numeric Relational Domains to Algebraic Data Types (extended version)

We present RAND, a relational abstract domain that expresses relations between values of non-recursive algebraic data types (ADTs), and numeric relations between their scalar parts. RAND is parametrised on a user-provided numeric relational domain, that we lift to pairs of variables and projection paths. It is constructed as a disjunctive completion of a reduced product of domains for numeric relations, for equalities, and for cases of variant constructors. Using RAND, we define a modular, inter-procedural, relational analysis for a while language with ADTs and function calls. The analysis computes function summaries, that describe relations between the inputs of programs and their outputs