/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml | 75 (* If we are code-generating a function immediately we make a one-word
|
H A D | CODETREE_SIMPLIFIER.sml | 133 compiler was compiled on. The ML word length will be the same because 330 Check that this is a word object and that the offset is within range. 361 used to load the string length word so we can use that. *) 1294 The base address for C memory operations is a LargeWord.word value i.e. 1400 (* Check that we have a valid value to add to a large word. 1407 val l: LargeWord.word = RunCall.unsafeCast c 1691 For this to work all loads from the stack must use native word length. *)
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_disassemblerLib.sml | 87 l |> List.map term_to_string |> commy |> directive_line "word" 850 directive_line "word" ("0x" ^ c ^ "6000010") 853 | "Encoding_Thumb2" => directive_line "word" "0xF7F0A000"
|
H A D | arm_parserLib.sml | 469 (n |> fcpLib.index_to_num |> Arbnum.toString) ^ "-bit word") 481 (n |> fcpLib.index_to_num |> Arbnum.toString) ^ "-bit word") 1792 "branch offset not half-word aligned") 1801 ("arm_parse_branch_target", "branch offset not word aligned") 1828 "branch offset not half-word aligned") 1844 ("arm_parse_branch_target", "branch offset not word aligned") 1885 "branch offset not word aligned") 1909 "branch offset not half-word aligned") 1954 ("arm_parse_cbz_cbnz", "offset not half-word aligned") 2793 ("arm_parse_mode3_dual_offset", "offset must be word aligne [all...] |
H A D | arm_decoderScript.sml | 25 val _ = type_abbrev_pp ("word1", ``:1 word``); 26 val _ = type_abbrev_pp ("word10", ``:10 word``); 27 val _ = type_abbrev_pp ("word11", ``:11 word``);
|
/seL4-l4v-master/HOL4/examples/PSL/experimental-semantics/ |
H A D | WeakPSLUnclockedSemanticsScript.sml | 63 (* we let \epsilon be the empty (neutral) word *) 224 # Weak/neutral word definition 308 (* Weaken a word *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Socket.sml | 262 (* Get the error state as an OS.syserror value. This is a SysWord.word value. *) 264 val sysGetError: OS.IO.iodesc -> SysWord.word = 267 fun getAndClearError(SOCK s): SysWord.word = sysGetError s
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | stateLib.sml | 330 "word" ^ Arbnum.toString (fcpSyntax.dest_numeric_type n) 1285 (List.map f [`\n : 'a word. n + z`, `\n : 'a word. z + n`, 1286 `\n : 'a word. n - z`, `\n : 'a word. z - n`])
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | extendTranslateScript.sml | 1691 Define `word_encode (:'b) (x:'b word) = int (sw2i x)`; 1693 Define `word_decode (:'b) x = (i2sw (sexp_to_int x)) : 'b word`; 1865 ``!a b. word_encode (:'a) (a && b : 'a word) = 1941 acl2_logbitp (nat b) (word_encode (:'a) (a:'a word)))``, 2005 ``bool (a > b) = bool (b < a : 'a word)``, 2009 ``bool (a >= b) = bool (b <= a : 'a word)``, 2021 ``nat (w2n a) = nat (i2n (sw2i (a:'a word)) (dimindex (:'a)))``,
|
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_evalScript.sml | 385 `!a:'a word b. (a = n2w b) = (w2n a = b MOD dimword (:'a))`, 508 `!w:'a word i h. 509 (h + 1 - l < i) /\ i < dimindex(:'b) ==> ~((((h >< l) w):'b word) ' i)`,
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_decoderScript.sml | 26 val _ = type_abbrev_pp ("word1", ``:1 word``); 27 val _ = type_abbrev_pp ("word10", ``:10 word``); 28 val _ = type_abbrev_pp ("word11", ``:11 word``);
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | Normal.sml | 145 if is_word_literal t andalso not (is_8bit_literal t) then REFL exp (* over 8-bit word constants *)
|
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/ |
H A D | ExampleScript.sml | 164 (* val _ = Datatype `Lexicon = <| word : string ; category : 'a Form |>`; *)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/step/ |
H A D | arm8_stepScript.sml | 248 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)`
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | MMU_SetupScript.sml | 424 (* predicate "word aligned around address add is readable" *)
|
/seL4-l4v-master/HOL4/examples/PSL/regexp/ |
H A D | regexpScript.sml | 236 (* sem r w means regular expression r matches word w (represented as a list) *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Bitmap.sml | 250 first word is less than the overall size. There are
|
H A D | DeviceBase.sml | 512 fun devModeSize({driverPrivate: Word8Vector.vector, ...}: DEVMODE): word =
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_bytecode_stepScript.sml | 223 |> DISCH ``(w2w:29 word->word32) j = n2w i`` 227 |> DISCH ``EL (w2n ((n2w i):29 word)) (xs ++ y::ys:SExp list) = EL i xs`` 232 |> DISCH ``(w2w:29 word->word32) j = n2w i`` 233 |> DISCH ``(w2n:29 word->num) j = i``
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_Lib.sml | 83 val any_b2w_ss = eval_term_ss "any_b2w" ``(b2w I xs):'a word``
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Lib.sml | 85 val any_b2w_ss = eval_term_ss "any_b2w" ``(b2w I xs):'a word``
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Numerics.sml | 12 type word8 = Word8.word;
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairTools.sml | 119 * "free" (which is thus probably the wrong word to use).
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/prog/ |
H A D | mips_progLib.sml | 27 val word = wordsSyntax.mk_int_word_type 32 value
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | bootup.tex | 192 \texttt{seL4\_Uint8[]} & \texttt{padding} & manual padding so final struct is a multiple of the word size \\
|