Searched refs:ov (Results 1 - 6 of 6) sorted by relevance

/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DrulesScript.sml499 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 DCFL_RulesScript.sml501 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 DrulesScript.sml500 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 Dbdd.h583 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 DPrim_rec.sml912 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 DpatternMatchesLib.sml1467 let val ov = pairSyntax.strip_pair vars_tm value
1468 in (vars_tm, ov @ new_col_vars) end

Completed in 82 milliseconds