Searched refs:rem (Results 1 - 25 of 60) sorted by relevance

123

/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/
H A DDataIn.c465 rem member in struct:__anon12
476 rem member in struct:__anon13
488 rem member in struct:__anon14
H A DEventTo.c2029 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 DmlibArbint.sml68 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 DmlibArbint.sig28 val rem : (int * int) -> int value
H A DmlibOmegaint.sig25 val rem : (int * int) -> int value
H A DmlibArbnum.sml74 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 DArbintcore.sml68 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 DArbintcore.sig26 val rem : (int * int) -> int value
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/
H A DwinNT-systeml.sml86 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 Dbvec.h97 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 Dbvec.c780 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 Dx86_encodeLib.sml127 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 DnumML.sml5 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 DArbintcore.sig28 val rem : (int * int) -> int value
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DwinNT-systeml.sml127 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 Dx64_encodeLib.sml175 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 DInt32.sml53 val rem = check o rem value
H A DINTEGER.sml36 val rem : (int * int) -> int value
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/
H A DBitsN.sml86 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 Dx64_codegenLib.sml358 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 Dgr_t.sml172 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 Dgr_t.sml172 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 Dgr_t.sml172 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 DintegerScript.sml2396 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 Dmuddy.c953 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);

Completed in 240 milliseconds

123