/seL4-l4v-10.1.1/seL4/src/api/ |
H A D | faults.c | 84 for (i = 0; i < MIN(length, n_msgRegisters); i++) { 107 for (i = 0; i < MIN(length, n_msgRegisters); i++) { 132 copyMRsFaultReply(sender, receiver, MessageID_Syscall, MIN(length, n_syscallMessage)); 136 copyMRsFaultReply(sender, receiver, MessageID_Exception, MIN(length, n_exceptionMessage));
|
/seL4-l4v-10.1.1/HOL4/src/emit/MLton/ |
H A D | numML.sml | 3 nonfix MOD DIV DIVMOD findq LEAST WHILE MAX MIN FUNPOW FACT ODD EVEN 93 fun MIN x y = (if < x y then x else y) function
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/metag/ |
H A D | ffi.c | 30 #define MIN(a,b) (((a) < (b)) ? (a) : (b)) macro 96 return ALIGN(MIN(stack - argp, 6*4), 8);
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | kernel.h | 175 #define MIN(a,b) ((a) < (b) ? (a) : (b)) macro
|
H A D | reorder.c | 477 maxAllowed = MIN(best/5+best, bddmaxnodesize-bddmaxnodeincrease-2); 511 maxAllowed = MIN(best/5+best, 539 maxAllowed = MIN(best/5+best, 965 levels[n].size = MIN(levels[n].maxsize, (levels[n].nodenum*5)/4); 1377 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size/2); 1379 levels[var1].size = MIN(levels[var1].maxsize, levels[var1].size*2);
|
H A D | bvec.c | 274 int minnum = MIN(bitnum, v.bitnum); 920 int n, minnum = MIN(e.bitnum,pos);
|
/seL4-l4v-10.1.1/seL4/include/ |
H A D | util.h | 19 #define MIN(a,b) (((a)<(b))?(a):(b)) macro
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_coretypesScript.sml | 231 (x >> shift, x ' (MIN (dimindex(:'a) - 1) (shift - 1)))`; 367 val MIN_LEM = Q.prove(`!a b. MIN a (MIN a b) = MIN a b`, SRW_TAC [] [MIN_DEF]);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_coretypesScript.sml | 235 (x >> shift, x ' (MIN (dimindex(:'a) - 1) (shift - 1)))`; 371 val MIN_LEM = Q.prove(`!a b. MIN a (MIN a b) = MIN a b`, SRW_TAC [] [MIN_DEF]);
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | wordsScript.sml | 188 (FCP i. l <= i /\ i <= MIN h ^HB /\ w ' i):'a word` 192 (FCP i. i + l <= MIN h ^HB /\ w ' (i + l)):'a word` 196 (FCP i. l <= MIN h ^HB /\ w ' (MIN (i + l) (MIN h ^HB))):'a word` 1306 (n2w (SLICE (MIN h ^HB) l n)):'a word`, 1311 (n2w (BITS (MIN h ^HB) l n)):'a word`, 1312 FIELD_WORD_TAC \\ Cases_on `i + l <= MIN h ^HB` 1328 n2w (SIGN_EXTEND (MIN (SUC h) (dimindex(:'a)) - l) (dimindex(:'a)) 1329 (BITS (MIN [all...] |
H A D | alignmentScript.sml | 149 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`,
|
/seL4-l4v-10.1.1/HOL4/examples/dev/booth/ |
H A D | boothScript.sml | 132 `MIN HB 1 = 1`, 151 `(!x t. MIN x (x - 2 + 2 * (t + 1)) = x) /\ 152 (!x t. MIN x (x + 2 * (t + 1)) = x)`, 197 `!t x. 2 * (t + 1) <= x + 1 ==> (MIN x (2 * t + 1) = 2 * t + 1)`,
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | arithmeticScript.sml | 2920 val MIN = new_definition("MIN_DEF", ���MIN m n = if m < n then m else n���); value 2930 ���!m n. MIN m n = MIN n m���, 2931 ARW [MIN] THEN FULL_SIMP_TAC bool_ss [NOT_LESS] THEN 2940 ���!m n p. MIN m (MIN n p) = MIN (MIN m n) p���, 2941 SIMP_TAC bool_ss [MIN] THE [all...] |
H A D | numSyntax.sml | 34 val min_tm = prim_mk_const {Name="MIN", Thy="arithmetic"}
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | treeScript.sml | 264 (MIN_LIST (t::l) = FOLDR MIN t l)` 270 (!n ns. (MIN_LIST (n::ns) = if (ns = []) then n else MIN n (MIN_LIST ns))) /\ 292 ``(MIN (SUC n1) (SUC n2) = SUC (MIN n1 n2)) /\
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | updateScript.sml | 58 let j = MIN n lx in
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | selftest.sml | 219 (* arithmetic operators: SUC, +, -, *, /, DIV, MOD, ABS, MIN, MAX *) 282 (``MIN (x:num) y <= x``, [thm_AUTO, thm_YO]), 283 (``MIN (x:num) y <= y``, [thm_AUTO, thm_YO]), 284 (``(z:num) < x /\ z < y ==> z < MIN x y``, [thm_AUTO, thm_YO]), 285 (``MIN (x:num) y < x``, [sat_YO, sat_Z3, sat_Z3p]), 286 (``MIN (x:num) 0 = 0``, [thm_AUTO, thm_YO]),
|
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | semantics.tex | 369 \subsection{The theory {\tt MIN}} 372 The {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by: 374 \theory{MIN} = 381 Since the theory \theory{MIN} has a signature consisting only of 385 Although the theory \theory{MIN} contains only the minimal standard 391 In the implementation, the theory \theory{MIN} is given the name 400 structure as \theory{MIN}. Its signature contains the constants in 401 \theory{MIN} an [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/ |
H A D | semantics.tex | 369 \subsection{La teoria {\tt MIN}} 372 La {\it teoria minimale\/}\index{MIN@\ml{MIN}}\index{minimal theory, della logica HOL@minimal theory, della logica \HOL{}} \theory{MIN} � definita da: 374 \theory{MIN} = 381 Dal momento che la teoria \theory{MIN} ha una firma che consiste solo di 385 Bench� la teoria \theory{MIN} contiene solo la sintassi standard 391 Nell'implementazione, alla teoria \theory{MIN} � dato il nome 400 di tipo di \theory{MIN}. La sua firma contiene le costanti in 401 \theory{MIN} [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/ |
H A D | multScript.sml | 60 `!x t. 0 < t ==> (MIN 31 (2 * t + 29) = 31)`, 168 `!x t. 0 < t ==> (MIN x (x - 2 + 2 * t) = x)`, 387 `!h m l n. SLICE h l (BITS m 0 n) = SLICE (MIN h m) l n`,
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibUseful.sml | 52 val MIN = 1.0; value 60 if t > MIN then (t / Real.fromInt n, res) else several n t f a
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | indexedListsScript.sml | 296 ���!f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)���,
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Useful.sml | 63 val MIN = 1.0; value 71 if t > MIN then (t / Real.fromInt n, res) else several n t f a
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 857 val MIN = 1.0; value 865 if t > MIN then (t / Real.fromInt n, res) else several n t f a
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 857 val MIN = 1.0; value 865 if t > MIN then (t / Real.fromInt n, res) else several n t f a
|