/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/ |
H A D | armScript.sml | 370 let word = if R then SPSR_READ psr mode else CPSR_READ psr in 371 ARM (REG_WRITE (INC_PC reg) mode Rd word) psr`;
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | armScript.sml | 416 let word = if R then SPSR_READ r.psr mode else CPSR_READ r.psr in 417 <| reg := REG_WRITE (INC_PC r.reg) mode Rd word; psr := r.psr |>`;
|
H A D | arm_rulesScript.sml | 65 `!a. ~(a = UINT_MAXw:'a word) ==> w2n a + 1 < dimword(:'a)`, 189 ``!i n. i < dimindex (:'a) ==> (((n2w n):'a word) ' i = BIT i n)``;
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | tutorial.ml | 278 (* A word on constructors.... *) 760 val wordp_def = flatten_fcp_recognizers (K "wordp") ``:'a word``;
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/ |
H A D | lisp_consScript.sml | 152 (ref_heap_addr (H_DATA (INR (v:29 word))) = w2w v << 3 !! 3w)`; 158 ``!m k. ((n2w m):'a word) << k = n2w (m * 2 ** k)``,
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/ |
H A D | prog_armScript.sml | 651 ``!k b f. (k :+ b) ((FCP i. f i):'a word) = (FCP i. if i = k then b else f i):'a word``,
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | prog_x86Script.sml | 844 ``!s:'a word set. FINITE s``, 870 (INST_TYPE [``:'a``|->``:'a word``] FINITE_INDUCT));
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | prog_x64Lib.sml | 50 val word2bytes_lemma = CONJ (EVAL ``word2bytes 2 (w:'a word)``) 51 (EVAL ``word2bytes 4 (w:'a word)``)
|
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | debug.c | 1078 ksKernelEntry.word = fault_vaddr; 1231 /* Don't attempt to shift beyond end of word. */
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automationLib.sml | 134 (���:word64���,���word:word64->v���), 135 (���:word4���,���word:word4->v���),
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 492 the second word. Must pass [] as the polyVars otherwise 956 by generating a word on the heap. The address of this word 958 bindings i.e. exception ex=ex' merely copy the word from 973 mutable word which acts as a token. It is a
|
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 496 val _ = syntax_error (arity <= 0) ("Variable '"^var_name^"' is not of type bool or a word type!");
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Window.sml | 64 | SWP_OTHER of Word32.word
|
/seL4-l4v-master/HOL4/src/res_quan/Manual/ |
H A D | description.tex | 123 {\tt word} to model bit vectors.}
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 281 | armML.DataProcessing (armML.Byte_Reverse_Word _) => "byte reverse word"
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | selftest.sml | 13 val _ = set_trace "notify word length guesses" 0;
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_initScript.sml | 59 val tms = find_terml (can (match_term ``((7 >< 0) (w:'a word)):word8``)) (concl th)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Int.sml | 99 val fixedIntAsWord: FixedInt.int -> word = RunCall.unsafeCast
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sml | 26 type w64 = Word64.word;
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | ipc.tex | 126 word chosen by the invoker of the \emph{mint} operation. When a message is sent to an endpoint using a badged
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/prog/ |
H A D | riscv_progLib.sml | 32 val word = wordsSyntax.mk_int_word_type 32 value
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 45 updates when the indices are integer or word literals *) 48 pats = [``(x :'a word) = y``], conv = wordsLib.word_EQ_CONV}),
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
H A D | binomial.tex | 16 % \self{} is one word denoting this document, such as "article" or "chapter" 603 is commutative. The word ring is used in the remainder of this \self{}
|
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/ |
H A D | binomial.tex | 16 % \self{} is one word denoting this document, such as "article" or "chapter" 603 is commutative. The word ring is used in the remainder of this \self{}
|
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | waaSimplScript.sml | 91 reduced_E run trans word (i,q) = 92 let a = $@ (\a. (a,run.E (i,q)) ��� trans q ��� at word i ��� a)
|