/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/ |
H A D | DataIn.c | 465 rem member in struct:__anon12 476 rem member in struct:__anon13 488 rem member in struct:__anon14
|
H A D | EventTo.c | 2029 rem member in struct:__anon39 2040 rem member in struct:__anon40 2052 rem member in struct:__anon41
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibArbint.sml | 68 infix 7 quot rem 75 fun ((true, n1) rem (true, n2)) = (true, n1 mmod n2) 76 | ((true, n1) rem (false, n2)) = norm_zeros (false, n1 mmod n2) 77 | ((false, n1) rem (true, n2)) = norm_zeros (false, n1 mmod n2) 78 | ((false, n1) rem (false, n2)) = (true, n1 mmod n2) 80 fun quotrem(i,j) = (i quot j, i rem j)
|
H A D | mlibArbint.sig | 28 val rem : (int * int) -> int value
|
H A D | mlibOmegaint.sig | 25 val rem : (int * int) -> int value
|
H A D | mlibArbnum.sml | 74 val rem = n mod BASE value 76 rem::(if dividend > 0 then fromInt dividend else []) 103 val (carry, rem) = if xyc >= BASE then (true, Int.-(xyc, BASE)) 106 rem::(addwc xs ys carry) 160 val (rem, carry) = (Int.mod(newx, BASE), Int.div(newx,BASE)) value 162 if carry = 0 then rem::f xs 163 else rem::(f xs + [carry])
|
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
H A D | Arbintcore.sml | 68 infix 7 quot rem 75 fun ((true, n1) rem (true, n2)) = (true, n1 mmod n2) 76 | ((true, n1) rem (false, n2)) = norm_zeros (false, n1 mmod n2) 77 | ((false, n1) rem (true, n2)) = norm_zeros (false, n1 mmod n2) 78 | ((false, n1) rem (false, n2)) = (true, n1 mmod n2) 80 fun quotrem(i,j) = (i quot j, i rem j)
|
H A D | Arbintcore.sig | 26 val rem : (int * int) -> int value
|
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 86 output "rem The bare HOL script\n"; 87 output "rem (automatically generated by HOL configuration)\n\n"; 105 output "rem The HOL script (with quote preprocessing)\n"; 106 output "rem (automatically generated by HOL configuration)\n\n";
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bvec.h | 97 extern int bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem); 98 extern int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem); 164 friend int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem); 165 friend int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem); 241 inline int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem) argument 242 { return bvec_divfixed(e.roots, c, &res.roots, &rem.roots); } 244 inline int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem) argument 245 { return bvec_div(l.roots, r.roots, &res.roots, &rem.roots); }
|
H A D | bvec.c | 780 PROTO {* int bvec_div(bvec e, int c, bvec *res, bvec *rem) *} 784 {\tt rem}. Both vectors should be initialized as the function 790 int bvec_divfixed(bvec e, int c, bvec *res, bvec *rem) argument 808 *rem = remainder; 833 PROTO {* int bvec_div(bvec l, bvec r, bvec *res, bvec *rem) *} 837 {\tt rem}. Both vectors should be initialized as the function 848 bvec rem; local 857 rem = bvec_coerce(bitnum, left); 868 bdd divLteRem = bdd_addref( bvec_lte(div, rem) ); 869 bvec remSubDiv = bvec_sub(rem, di [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sml | 127 fun rem [] b ys = rev ys function 128 | rem (x::xs) b ys = 129 if x = #"[" then rem xs true (x::ys) else 130 if x = #"]" then rem xs false (x::ys) else 131 if x = #" " then if b then rem xs b ys else rem xs b (x::ys) else 132 rem xs b (x::ys) 133 val s = implode (rem (explode s) false [])
|
/seL4-l4v-10.1.1/HOL4/src/emit/MLton/ |
H A D | numML.sml | 5 quot rem + - ^ @ <> > < >= <= := o before; 18 fun mod2 x = LargeInt.rem(x, TWO) 118 fun MOD m n = LargeInt.rem(m, n)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Arbintcore.sig | 28 val rem : (int * int) -> int value
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | winNT-systeml.sml | 127 output "rem The bare HOL script\n"; 128 output "rem (automatically generated by HOL configuration)\n\n"; 146 output "rem The HOL script (with quote preprocessing)\n"; 147 output "rem (automatically generated by HOL configuration)\n\n";
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_encodeLib.sml | 175 fun rem [] b ys = rev ys function 176 | rem (x::xs) b ys = 177 if x = #"[" then rem xs true (x::ys) else 178 if x = #"]" then rem xs false (x::ys) else 179 if x = #" " then if b then rem xs b ys else rem xs b (x::ys) else 180 rem xs b (x::ys) 181 val s = implode (rem (explode s) false [])
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Int32.sml | 53 val rem = check o rem value
|
H A D | INTEGER.sml | 36 val rem : (int * int) -> int value
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
H A D | BitsN.sml | 86 IntInf.rem (IntInf.~>> (a, Word.fromLargeInt n), 2) = 1 87 fun lsb (B (a, _)) = IntInf.rem (a, 2) = 1 211 fun op rem (a, b as B (_, s)) = fromInt (IntInf.rem (toInt a, toInt b), s)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegenLib.sml | 358 fun rem (FUN_VAL tm) = FUN_VAL tm function 359 | rem (FUN_COND x) = FUN_COND x 360 | rem (FUN_IF (tm,t1,t2)) = FUN_IF (tm,rem t1,rem t2) 361 | rem (FUN_LET (tm1,tm2,t)) = let 362 val t = rem t 366 val t = rem t
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr_t.sml | 172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) 173 val t3 = remFromLab (t2,n,p',T3) (* rem. n from each suc-list of p *) 261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) 262 val t3 = remFrom (t2,n,p',T3) (* rem. n from each suc-list of p *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr_t.sml | 172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) 173 val t3 = remFromLab (t2,n,p',T3) (* rem. n from each suc-list of p *) 261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) 262 val t3 = remFrom (t2,n,p',T3) (* rem. n from each suc-list of p *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 172 val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *) 173 val t3 = remFromLab (t2,n,p',T3) (* rem. n from each suc-list of p *) 261 val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *) 262 val t3 = remFrom (t2,n,p',T3) (* rem. n from each suc-list of p *)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | integerScript.sml | 2396 Define integer rem(ainder) and quot(ient) functions. 2404 val _ = print "Define integer rem(ainder) and quot(ient) functions\n" 2540 (* define rem *) 2550 val _ = set_fixity "rem" (Infixl 650); 2551 val _ = overload_on("rem", ``int_rem``); 2555 ``!p q. ~(q = 0) ==> (&p rem &q = &(p MOD q))``, 2597 ``!q. ~(q = 0) ==> !p. (p = p quot q * q + p rem q) /\ 2598 (if 0 < p then 0 <= p rem q else p rem q <= 0) /\ 2599 ABS (p rem [all...] |
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/ |
H A D | muddy.c | 953 BVEC res, rem; local 955 bvec_divfixed(BVEC_val(s1), Int_val(con), &res, &rem); local 958 Field(result[0], 0) = mlbdd_make_bvec(rem); 966 BVEC res, rem; local 968 bvec_div(BVEC_val(s1), BVEC_val(s2), &res, &rem); local 971 Field(result[0], 0) = mlbdd_make_bvec(rem);
|