fact: Definition trinode (sh: share) (p: addr) (dlr: bool * addr * addr): mpred := match dlr with | (d, l, r) => data_at sh node_type (Vint (Int.repr (if d then 1 else 0)), (pointer_val_val l, pointer_val_val r)) (pointer_val_val p) end.
imports: CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.mark.env_mark_bin CertiGraph.floyd_ext.share