fact: Definition main_spec := DECLARE _main WITH gv : globals PRE [] main_pre prog tt gv POST [ tint ] PROP() LOCAL (temp ret_temp (Vint (Int.repr (1+2+3+4)))) SEP(TT).
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon