fact: Definition desugarPure (specs:list FULL_SPEC_CASE.t) (m:METHOD.t) : list FULL_SPEC_CASE.t := let addBody2 clause1 clause2 spec := addBody (addBody spec clause1) clause2 in let div := divergesC false (: false' :)%jml in let ass := match METHOD.kind m with | Constructor => assignableC false (: StoreRefs [AllFieldsRef ThisRef] :)%jml | _ => assignableC false (: \nothing :)%jml end in let defaultCase := GENERIC_SPEC_CASE.Build_t nil nil nil (inl _ (div :: ass :: nil)) in let defaultSpecs := FULL_SPEC_CASE.Build_t lightweight None false false defaultCase in match METHOD.isPure m, specs with | false, _ => specs | true, nil => defaultSpecs :: nil | true, _ => map (addBody2 ass div) specs end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)