fact: Fixpoint StoreRefPrefix2Object (fr : Frame.t) (sr : StoreRefPrefix) : Object := match sr with | ThisRef => match Frame.this fr with | Some loc => loc | _ => UndefinedObject end | ParamRef p => match ParamDict.get (Frame.params fr) p with | Some (Ref loc) => loc | _ => UndefinedObject end | PathRef target fsig => match Heap.get fr@preheap (Heap.InstanceField (StoreRefPrefix2Object fr target) fsig) with | Some (Ref loc) => loc | _ => UndefinedObject end end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)