fact: Definition vgamma2cdata (dlr : bool * addr * addr) : reptype node_type := match dlr with | (d, l, r) => (Vint (Int.repr (if d then 1 else 0)), (pointer_val_val l, pointer_val_val r)) end.
imports: CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.dispose.env_dispose_bin CertiGraph.floyd_ext.share