Lines Matching refs:ov
500 VSPEC ir (pre_p,post_p) stk (iv,f,ov) =
501 PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov))
508 `!ir stk iv f ov g iv'.
509 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv))
511 VSPEC ir (pre_p,post_p) stk (iv', g, ov)`,
528 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov.
530 VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\
531 VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st)
533 VSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk (iv, (\v.if cond_f v then f1 v else f2 v), ov)`,
557 `!ir pre_p pre_p' post_p stk iv f ov.
559 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. pre_p' st ==> pre_p st) ==>
560 VSPEC ir (pre_p',post_p) stk (iv,f,ov)`,
567 `!ir pre_p post_p post_p' stk iv f ov.
569 PSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. post_p st ==> post_p' st) ==>
570 PSPEC ir (pre_p,post_p') stk (iv,f,ov)`,
581 `!ir pre_p post_p stk iv f ov e g.
582 VSPEC ir (pre_p,post_p) (e::stk) (iv,f,ov) /\
584 VSPEC ir (pre_p,post_p) stk (PR(iv,e), g, PR(ov,e))`,
595 `!ir pre_p post_p stk iv f ov e.
596 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ V_intact(pre_p, post_p, e)
598 VSPEC ir (pre_p,post_p) (e::stk) (iv, f, ov)`,