fact: Definition list_rep sh size l contents_mat index := let mylist := (Znth index contents_mat) in data_at sh (tarray tuint size) (map Vint (map Int.repr mylist)) (list_address l index size).
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon