Open igcontreras opened 4 years ago
Obtaining a node in a graph that corresponds to a global variable introduces an empty node in the graph that is not linked to anything.
short2.pp.ms.o.bc.zip
To reproduce this:
$ seadsa --sea-dsa-type-aware --sea-dsa=cs --sea-dsa-color-func-sim-dot --sea-dsa-dot short2.pp.ms.o.bc $ dot -Tpdf main.TD.mem.dot -o main.TD.mem.pdf $ dot -Tpdf main.mem.dot -o main.mem.pdf
main.TD.pdf and main.pdf represent the same graph, main.TD.pdf is colored according to the simulation relation of the bottom-up graph. When coloring, the same graph is used for both: https://github.com/seahorn/sea-dsa/blob/24d8ad338387b5f90d89fe4ec3b968b7e4b01610/lib/seadsa/DsaPrinter.cc#L745 But main.pdf is printed before the simulation and main.TD.pdf after.
main.pdf main.TD.pdf
Obtaining a node in a graph that corresponds to a global variable introduces an empty node in the graph that is not linked to anything.
short2.pp.ms.o.bc.zip
To reproduce this:
main.TD.pdf and main.pdf represent the same graph, main.TD.pdf is colored according to the simulation relation of the bottom-up graph. When coloring, the same graph is used for both: https://github.com/seahorn/sea-dsa/blob/24d8ad338387b5f90d89fe4ec3b968b7e4b01610/lib/seadsa/DsaPrinter.cc#L745 But main.pdf is printed before the simulation and main.TD.pdf after.
main.pdf main.TD.pdf