Lines Matching refs:function
290 (* the characteristic function *)
293 val f_c = mk_pabs (initV, subst rules (calculate_outs post_st outs)); (* the charateristic function *)
299 (* the stack function *)
317 (* Given an basic block, the charateristic function on inputs and outputs are derived by symbolic simulation *)
415 (* the characteristic function of SC *)
515 (* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *)
550 val cj_cond = subst rules instance1 (* the condition function *)
555 fun mk_cond_f cond_t ins = (* the condition function *)
616 (* the characteristic function *)
686 (* the characteristic function *)
890 (* Equivalence between the original function and the spec function *)
909 (print "Proving equivalence with input function\n";
912 val _ = print "! Equivalence proof between original function and\n";