The Undefined Domain: Precise Relational Information for Entities That Do Not Exist

摘要: Verification by static analysis often hinges on the inference of relational numeric information. In real-world programs, set active variables is not fixed for a given program point due to, instance, heap-allocated cells or recursive function calls. For these points, an invariant has to summarize values traces E where variable x exists and N does exist. Non-relational domains solve this problem copying all information in those N. Relational face challenge that relations between other cannot simply be replicated This work illustrates proposes general solution form co-fibered abstract domain forwards each operation operations child domain. By tracking which are undefined, it transparently stores suitable thus minimizing loss We present applications heap abstractions summaries.