fact: Definition graph1 : graph := [ (p1, (Vint (Int.repr 2), (nullval,nullval))); (p2, (Vint (Int.repr 3), (p1,p1))); (p3, (Vint (Int.repr 1), (p1,p2))) ].
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread