fact: Definition StoreRef2Location (p : Program) (fr : Frame.t) (sr : StoreRef) : LocSet.t := match sr with | StaticFieldRef fsig => LocSet.singleton (Heap.StaticField fsig) | FieldRef target fsig => LocSet.singleton (Heap.InstanceField (StoreRefPrefix2Object fr target) fsig) | AllFieldsRef target => AllAmOfObject p fr@preheap (StoreRefPrefix2Object fr target) end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)