fact: Definition SpaceAdjMatGraph' sh g_contents gaddr : mpred := data_at sh (tarray tint (size * size)) (map Vint (map Int.repr g_contents)) gaddr.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat compcert.lib.Integers compcert.common.Values compcert.export.Clightdefs VST.veric.expr VST.veric.mpred VST.floyd.forward VST.zlist.sublist VST.floyd.field_at VST.floyd.coqlib3 VST.msl.iter_sepcon VST.msl.seplog CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph