fact: Definition EvalMethodInvocation (msig : MethodSignature) (target : option Expression) (actuals : list Expression) (st : State.t) : option Value := let pv := EvalParams (METHODSIGNATURE.parameters (snd msig)) actuals st in match target with | Some target' => match EvalRefExpression target' st with | Some target'loc => match Heap.typeof st@h target'loc with | Some (Heap.ObjectObject cn um) => match Lookup p cn (snd msig) with |Some (cn', m') => match PROG.class p cn with | Some c' => let params := lv2params m' ((l2v (Some target'loc))::pv) in let fr' := NewFrame m' params st in EvalPureMethod p c' m' st[fr:=fr'] | None => None end | _ => None end | _ => None end | None => None end | None => match PROG.class p (fst msig) with | Some c' => match findMethod p msig with | Some m' => let params := lv2params m' pv in let fr' := NewFrame m' params st in EvalPureMethod p c' m' st[fr:=fr'] | None => None end | None => None end end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)