fact: Definition InitState : State.t := let frameadds := FrameAdds.make LocSet.empty ObjSet.empty (InitHeap, ParamDict.empty) VarDict.empty in let frame := Frame.build InitMethod ParamDict.empty frameadds in State.build InitHeap frame Adds.singleton.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)