Searched refs:ov (Results 1 - 6 of 6) sorted by relevance
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | rulesScript.sml | 499 VSPEC ir (pre_p,post_p) stk (iv,f,ov) = 500 PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov)) 507 `!ir stk iv f ov g iv'. 508 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv)) 510 VSPEC ir (pre_p,post_p) stk (iv', g, ov)`, 527 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov. 529 VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\ 530 VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st) 532 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)`, 556 `!ir pre_p pre_p' post_p stk iv f ov [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFL_RulesScript.sml | 501 VSPEC ir (pre_p,post_p) stk (iv,f,ov) = 502 PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov)) 509 `!ir stk iv f ov g iv'. 510 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv)) 512 VSPEC ir (pre_p,post_p) stk (iv', g, ov)`, 529 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov. 531 VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\ 532 VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st) 534 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)`, 558 `!ir pre_p pre_p' post_p stk iv f ov [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | rulesScript.sml | 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 [all...] |
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bdd.h | 583 inline int bdd_setbddpair(bddPair *p, int ov, const bdd &nv) argument 584 { return bdd_setbddpair(p,ov,nv.root); }
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Prim_rec.sml | 912 val (ov,iv) = partition (C free_in ant) vs value 914 val thm2 = GENL ov (DISCH ant thm1) 916 val thm3 = SPECL iv (UNDISCH (SPECL ov (ASSUME asm)))
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 1467 let val ov = pairSyntax.strip_pair vars_tm value 1468 in (vars_tm, ov @ new_col_vars) end
|
Completed in 82 milliseconds