Searched defs:rv (Results 1 - 8 of 8) sorted by path

/seL4-l4v-master/HOL4/examples/HolCheck/
H A DcacheTools.sml456 val rv = snd(dest_comb mf) value
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DpolytypicLib.sml1768 val rv = mapfilter (fn vf => SPEC (rand vf) ( value
/seL4-l4v-master/HOL4/polyml/basis/
H A DIEEEReal.sml52 val rv = value
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Drealconv.cpp609 Bigint *rv; variable
2195 int rv = hi0bits(b->x[b->wds-1]) - 4; variable
2337 double rv; variable
2354 U *rv; CONST char *s0; BCinfo *bc; variable
2374 word0(rv) = (P+2) << Exp_shift; variable
2376 word1(rv) = 1; variable
2405 word0(rv) = (1 + bc->scale) << Exp_shift; variable
2407 word0(rv) = Exp_msk1; variable
2409 word1(rv) = 0; variable
2572 U aadj2, adj, rv, rv0; variable
2602 dval(&rv) = 0.; variable
2757 word0(&rv) = 0x7ff00000; variable
2758 word1(&rv) = 0; variable
2765 word0(&rv) = NAN_WORD0; variable
2766 word1(&rv) = NAN_WORD1; variable
2908 word0(&rv) = Big0; variable
2909 word1(&rv) = Big1; variable
2912 word0(&rv) = Exp_mask; variable
2913 word1(&rv) = 0; variable
2954 word0(&rv) = Big0; variable
2955 word1(&rv) = Big1; variable
2958 word0(&rv) += P*Exp_msk1; variable
2964 dval(&rv) /= tens[i]; variable
2982 word0(&rv) = (P+2)*Exp_msk1; variable
2984 word0(&rv) &= 0xffffffff << (j-32); variable
2987 word1(&rv) &= 0xffffffff << j; variable
3002 dval(&rv) = 0.; variable
3006 word0(&rv) = Tiny0; variable
3007 word1(&rv) = Tiny1; variable
3208 dval(&rv) += adj.d*ulp(&rv); variable
3230 word0(&rv) += P*Exp_msk1; variable
3233 dval(&rv) += adj.d; variable
3303 word1(&rv) = 0; variable
3352 word0(&rv) = L | Bndry_mask1; variable
3353 word1(&rv) = 0xffffffff; variable
3379 dval(&rv) += sulp(&rv, &bc); variable
3458 dval(&rv) += adj.d; variable
3464 word1(&rv) = Big1; variable
3468 word0(&rv) += P*Exp_msk1; variable
3483 dval(&rv) += adj.d; variable
3496 dval(&rv) += adj.d; variable
3667 char *rv, *t; variable
[all...]
/seL4-l4v-master/HOL4/src/HolSat/
H A DminisatResolve.sml18 let val rv = Array.sub(sva,n+1) value
/seL4-l4v-master/HOL4/src/num/reduce/src/
H A DArithconv.sml229 val rv = mk_var {Name= "r", Ty=num}; value
/seL4-l4v-master/HOL4/src/parse/
H A DAbsyn.sml82 val (rv, body) = dpa body value
/seL4-l4v-master/HOL4/src/coretypes/
H A DpairSyntax.sml235 val (rv, body) = dest_pabs body value

Completed in 123 milliseconds