fact: Definition initialise_matrix_spec := DECLARE _initialise_matrix WITH arr : val, old_contents: list Z, a: Z PRE [tptr tint, tint] PROP ( writable_share Tsh; Zlength old_contents = Z.mul size size; repable_signed a; 0 < size <= Int.max_signed; size * (4 * size) <= Ptrofs.max_signed ) PARAMS ( arr ; Vint (Int.repr a) ) GLOBALS () SEP (@SpaceAdjMatGraph' size CompSpecs Tsh old_contents arr) POST [ tvoid ] PROP () LOCAL () SEP (@SpaceAdjMatGraph' size CompSpecs Tsh (repeat a (Z.to_nat (Z.mul size size))) arr).
imports: CertiGraph.prim.prim_env CertiGraph.priq.priq_arr_specs CertiGraph.graph.MathUAdjMatGraph CertiGraph.prim.prim_constants CertiGraph.graph.SpaceUAdjMatGraph2 CertiGraph.prim.prim2