| /seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
| H A D | armScript.sml | 437 and rs = REG_READ reg mode Rs value
[all...] |
| H A D | coreScript.sml | 1036 and rs = REG_READ6 reg (DECODE_MODE m) (^Rg 11 8 ireg) in value
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/ |
| H A D | multScript.sml | 647 and rs = REG_READ6 reg nbs ((11 >< 8) ireg) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | armScript.sml | 476 and rs = REG_READ r.reg mode Rs value
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_encoderLib.sml | 966 let val (rs,typ,m) = dest_Mode1_register_shifted_register mode1 in value
|
| H A D | arm_parserLib.sml | 1535 let val (rs,typ,_) = dest_Mode1_register_shifted_register mode1 in value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | polytypicLib.sml | 3165 let val rs = guarenteed (map (rhs o snd o strip_forall) o strip_conj o snd o dest_imp_only) term value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | funCall.sml | 614 val rs = S.addList (S.empty regAllocation.intOrder, get_modified_regs ir0); value
[all...] |
| H A D | regAllocation.sml | 840 val rs = getModifiedRegs stms value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | funCall.sml | 464 val rs = S.addList (S.empty regAllocation.intOrder, get_modified_regs ir0); value
[all...] |
| H A D | regAllocation.sml | 840 val rs = getModifiedRegs stms value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | funCall.sml | 461 val rs = S.addList (S.empty regAllocation.intOrder, get_modified_regs ir0); value
[all...] |
| H A D | regAllocation.sml | 840 val rs = getModifiedRegs stms value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | SALGen.sml | 302 val rs = pre_process def value
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/ |
| H A D | CutFreeScript.sml | 381 val [rs, rbs, rd1, rd2, ls1, ls2, lbs1, lbs2, ld, cr1, cr2, se] = value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | stateLib.sml | 1703 val rs = mk_assign regs (pl, ql) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | reg_allocLib.sml | 194 val rs = zip vs xs @ zip (map (subst m) xs) vs value
201 val rs = forward rs [] value
207 val rs = in_tail rs value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 625 val rs = redexes result value
1273 val rs = redexes result value
1339 val rs = redexes s value
1391 val rs = redexes s value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | prog_ppcLib.sml | 33 val rs = find_terml (can (match_term ``PREAD_R x s``)) (concl th) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | prog_x86Lib.sml | 34 val rs = find_terml (fn tm => type_of tm = ``:Xreg``) (concl th) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | prog_x64Lib.sml | 54 val rs = find_terml (fn tm => type_of tm = ``:Zreg``) (concl th) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
| H A D | export_codeLib.sml | 60 val rs = map (word2string o snd) vs value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | export_codeLib.sml | 60 val rs = map (word2string o snd) vs value
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootParser.sml | 760 val rs = find_used_holvars res_varL (Redblackset.empty String.compare) t; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 527 val rs = (map (fn p => RW [ind_hyp] (SPEC p th) value
|