fact: Definition StaticDGs (p : Program) (f : Location) : list Location := match f with | Heap.InstanceField obj fsig => match findField p fsig with | Some f => let dgs := FIELD.dataGroups f in let dgs_static := filter (fun dg => negb (DATA_GROUP.isDynamic dg)) dgs in let dgfsig := flat_map DATA_GROUP.dataGroups dgs_static in map (Heap.InstanceField obj) dgfsig | _ => [] end | _ => [] end.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)