/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Random.sig | 1 (* Random -- random number generator *) 17 [generator] is the type of random number generators, here the 20 [newgenseed seed] returns a random number generator with the given seed. 22 [newgen ()] returns a random number generator, taking the seed from 25 [random gen] returns a random number in the interval [0..1). 30 [range (min, max) gen] returns an integral random number in the
|
H A D | SHA1_ML.sig | 4 * takes in stream state and an positive integer n specifying the number
|
/seL4-l4v-master/HOL4/src/num/theories/ |
H A D | Num_conv.sig | 3 (* DESCRIPTION : Signature for the alogical hack relating number *)
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | traps.S | 122 #define EXPAND_EXCEPT_1(number) \ 126 movq $0x##number, %rcx; \ 132 #define EXPAND_EXCEPT_0(number) \ 144 movq $0x##number, %rcx; \ 147 #define INT_HANDLE_COMMON_EXCEPT(number,except) _expand_except_(except)(number) 150 #define INT_HANDLER_COMMON(number,error_code,except) \ 151 .global int_##number; \ 152 .type int_##number, %function; \ 153 int_##number [all...] |
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_pseudoTools.sml | 2 (* Coversions for evaluating the pseudo-random number generator. *)
|
H A D | prob_pseudoScript.sml | 8 (* The definition of the pseudo-random number generator. *)
|
/seL4-l4v-master/l4v/misc/pysymbols/isasymbols/ |
H A D | isasymbols.py | 46 for number, line in enumerate(x.strip() for x in 60 number) 71 number) 87 (number, k))
|
/seL4-l4v-master/seL4/tools/hardware/ |
H A D | irq.py | 18 its number. ''' 20 # pop the right number of irq cells 124 # second cell: PPI or SPI number 130 number = data.pop(0) 136 number += 16 # SGI takes 0-15 138 number += 16 # PPI is 16-31 147 return number
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | locn.sig | 7 | LocA of int (* absolute line number in file (0-origin) *) 8 * int (* absolute column number in file (0-origin) *) 24 concatenated and given the number of the first fragment; the
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Waiting.sig | 21 (* s = the number of symbols in the clause *) 22 (* v = the number of distinct variables in the clause *) 23 (* l = the number of literals in the clause *)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Waiting.sig | 21 (* s = the number of symbols in the clause *) 22 (* v = the number of distinct variables in the clause *) 23 (* l = the number of literals in the clause *)
|
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 18 int starty,endy,number; field in class:TreeNode 58 number=num; 66 public int getNumber() { return number; } 101 if (number>=0) v.addElement(new Integer(number));
|
H A D | Vertex.java | 20 int number=-1; field in class:Vertex 52 /** internal number, for decoding / encoding etc. **/ 54 public int getNumber() { return number; } 56 public void setNumber(int n) { number=n; }
|
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 18 int starty,endy,number; field in class:TreeNode 58 number=num; 66 public int getNumber() { return number; } 101 if (number>=0) v.addElement(new Integer(number));
|
H A D | Vertex.java | 20 int number=-1; field in class:Vertex 52 /** internal number, for decoding / encoding etc. **/ 54 public int getNumber() { return number; } 56 public void setNumber(int n) { number=n; }
|
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | TEA.sml | 6 (* causes all bits of the key and data to be mixed repeatedly.The number of *) 56 (* Arbitrary number of cipher rounds *) 99 (* Arbitrary number of decipher rounds *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | holCheckTools.sml | 25 val ap = List.map (fn p => prop2ap p state) prop_tms (*FIXME: don't use abstraction if number of AP's is too high *) 35 (* return NONE if the number of atomic propositions is >= number of concrete state vars since abs won't help in that case*)
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sig | 32 count (* max number of cycles, -ve for unbounded *)
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_syntaxScript.sml | 22 exp = Const num (* constant number *)
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | holyHammer.sig | 8 val dep_flag : bool ref (* remove limits on the number of premises *)
|
/seL4-l4v-master/HOL4/examples/muddy/ |
H A D | bdd.sig | 154 number of nodes in the nodetable and cachesize is the fixed size of 160 The initial number of nodes is not critical for any bdd operation 167 [setvarnum num] is used to define the number of variables used in 169 increase the number of variables. num is the number of variables to 347 produced : total number of new nodes ever produced. 348 nodenum : currently allocated number of bdd nodes. 349 maxnodenum : user defined maximum number of bdd nodes. 350 freenodes : number of currently free nodes. 351 minfreenodes : minimum number o [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Time.sml | 53 uses a 64-bit number of 100ns ticks, Unix uses one word of seconds 55 arbitrary precision number for times with the actual resolution 61 (* Get the number of ticks per microsecond and compute the corresponding 77 (* The real representation is as a number of seconds. *) 100 (* Format as a fixed precision number. if n < 0 treat as n = 0. *) 104 (* The scanned string is a subset of the format of a real number. 106 number but it would probably be better to treat it as an integer. *)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 300 raise Fail "Bad number of arguments to `if' function." 311 raise Fail "Bad number of arguments to `subst' function." 322 raise Fail "Bad number of arguments to `patsubst' function." 332 raise Fail "Bad number of arguments to `protect' function." 336 raise Fail "Bad number of arguments to 'dprot' function." 339 raise Fail "Bad number of arguments to 'findstring' \ 351 raise Fail "Bad number of arguments to 'which' function" 358 raise Fail "Bad number of arguments to 'wildcard' function" 366 raise Fail "Bad number of arguments to 'shell' function"
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | more_listScript.sml | 92 (* For all lists of numbers l, the number of elements of value n *) 93 (* or more equals the number of elements of value n plus the *) 94 (* number of elements of value more than n. *)
|
/seL4-l4v-master/HOL4/examples/ |
H A D | Thery.sml | 76 Now consider cases on the number of coins of value 5. 84 Case: no coins of value 5. Now consider the number (j) of coins 148 (* Natural number version *)
|