Searched defs:rm (Results 1 - 18 of 18) sorted by path

/seL4-l4v-10.1.1/HOL4/developers/mlton-srcs/
H A DBinarymap.sml234 let fun rm E = raise NotFound function
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmScript.sml281 and rm = REG_READ (INC_PC reg) mode Rm value
438 and rm = REG_READ pc_reg mode Rm in value
[all...]
H A DlemmasScript.sml122 and rm = REG_READ (INC_PC r) m ((3 >< 0) i) in value
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DarmScript.sml323 and rm = REG_READ (INC_PC reg) mode Rm value
477 and rm = REG_READ r.reg mode Rm in value
[all...]
H A DsystemScript.sml592 and rm = REG_READ (INC_PC reg) mode (n2w Rm) in value
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_decoderScript.sml434 (let rdn = (3 :+ b7) (r 0) and rm = r4 3 in value
H A Darm_opsemScript.sml334 (address_mode1 ii thumb2 (Mode1_register imm5 type rm) = type
339 (address_mode1 ii thumb2 (Mode1_register_shifted_register rs type rm) = type
351 (address_mode2 ii indx add rn (Mode2_register imm5 type rm) = type
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_decoderScript.sml434 (let rdn = (3 :+ b7) (r 0) and rm = r4 3 in value
H A Darm_opsemScript.sml334 (address_mode1 ii thumb2 (Mode1_register imm5 type rm) = type
339 (address_mode1 ii thumb2 (Mode1_register_shifted_register rs type rm) = type
351 (address_mode2 ii indx add rn (Mode2_register imm5 type rm) = type
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/
H A Darm.sml4109 val rm = R m value
4130 val rm = R m value
4153 val rm = R m value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64.sml4264 val rm = BitsN.fromNat(Cast.ZregToNat rm,4) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/
H A Dx64_stepLib.sml430 val rm = value
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dx86_dep.cpp992 unsigned int rm = modrm & 7; local
/seL4-l4v-10.1.1/HOL4/src/1/
H A Dselftest.sml117 fun rm s = FileSys.remove ("scratchTheory." ^ s) function
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMetis.sml68 fun rm ns = function
/seL4-l4v-10.1.1/HOL4/src/num/termination/
H A DTotalDefn.sml58 fun rm x [] = [] function
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DInduction.sml126 fun rm x [] = [] | rm x (h::t) = if x=h then rm x t else h::rm x t; function
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/
H A DBinarymap.sml165 let fun rm E = raise NotFound function

Completed in 198 milliseconds