A Product of Shape and Sequence Abstractions

International audienceTraditional separation logic-based shape analyses utilize in-ductive summarizing predicates so as to capture general properties of thelayout of data-structures, to verify accurate manipulations of, e.g., variousforms of lists or trees. However, they also usually abstract away contentsproperties, so that they may only verify memory safety and invariance ofdata-structure shapes. In this paper, we introduce a novel abstract domainto describe sequences of values of unbounded size, and track constraintson their length and on extremal values contained in them. We define areduced product of such a sequence abstraction together with an existingshape abstraction so as to infer both shape and contents properties ofdata-structures. We report on the implementation of the sequence domain,its integration into a static analyzer for C code, and we evaluate its ability toverify partial functional correctness properties for list and tree algorithms