fact: Definition mallocN_spec := DECLARE _mallocN WITH sh: wshare, n:Z PRE [tint] PROP (0 <= n <= Int.max_signed) PARAMS (Vint (Int.repr n)) GLOBALS () SEP () POST [ tptr tvoid ] EX v: addr, PROP () LOCAL (temp ret_temp (pointer_val_val v)) SEP (data_at sh node_type (Vint (Int.repr 0), pointer_val_val null) (pointer_val_val v)).
imports: CertiGraph.unionfind.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_graph_glist