Oversharing with offset collapsed but types known

[igcontreras]

Program: oversharing.txt -- uploaded as txt because they dont allow .c or .i.

Steps to reproduce:

$ mv oversharing.txt oversharing.i
$ sea smt -O2 --horn-nondet-undef --sea-dsa-type-aware --dsa=sea-cs --horn-stats --horn-singleton-aliases=true --horn-ignore-calloc=true --horn-ignore-memset=true --horn-shadow-mem-optimize=false oversharing.i --oll=oversharing.ll
$ seadsa --sea-dsa-type-aware --sea-dsa=cs --sea-dsa-color-func-sim-dot --sea-dsa-dot oversharing.ll 
$ dot -Tpdf tulip_down.TD.mem.dot -o tulip_down.TD.mem.dot.pdf
$ dot -Tpdf tulip_down.BU.mem.dot -o tulip_down.BU.mem.dot.pdf

In the 2 pdfs produced, nodes with the same color in the BU are simulated by a node with the same color in the TD graph. The gray nodes in the TD graphs are not reachable if exploring it via the BU graph with the simulation.

Bottom-up graph:
tulip_down.BU.mem.dot.pdf

Top-down graph:
tulip_down.TD.mem.dot.pdf