| /seL4-l4v-master/seL4/src/arch/x86/machine/ |
| H A D | registerset.c | 18 context->registers[CS] = SEL_CS_3;
|
| /seL4-l4v-master/seL4/src/arch/x86/32/kernel/ |
| H A D | thread.c | 31 setRegister(tcb, CS, SEL_CS_0);
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | Tree.sml | 27 | CC | LS | HI | CS
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | Tree.sml | 26 and relop = EQ | NE | LT | GT | LE | GE | CC | LS | HI | CS
62 | CC | LS | HI | CS
|
| H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS
97 | print_cond (SOME CS) = "CS"
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | Tree.sml | 26 and relop = EQ | NE | LT | GT | LE | GE | CC | LS | HI | CS
62 | CC | LS | HI | CS
|
| H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS
97 | print_cond (SOME CS) = "CS"
|
| /seL4-l4v-master/seL4/src/arch/x86/64/kernel/ |
| H A D | thread.c | 37 setRegister(tcb, CS, SEL_CS_0);
|
| /seL4-l4v-master/seL4/include/arch/x86/arch/32/mode/machine/ |
| H A D | registerset.h | 49 /* 0x2C */ CS = 11, enumerator in enum:_register
|
| /seL4-l4v-master/HOL4/examples/computability/lambda/ |
| H A D | numsAsCompStatesScript.sml | 9 val _ = Datatype ���compstate = CS num���;
12 terminated (CS cs) ��� (pr_bnf [cs] = 1)
16 step1 (CS cs) = CS (pr_noreduct [cs])
24 ���cs. steps n (CS cs) = CS (pr_steps [n; cs])
34 cs_to_num (CS cs) = pr_forcenum [cs]
38 mk_initial_state i n = CS (pr_dAPP [i; pr_church [n]])
|
| /seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/machine/ |
| H A D | registerset.h | 63 CS = 20, /* 0xa0 */ enumerator in enum:_register
|
| /seL4-l4v-master/HOL4/src/simp/src/ |
| H A D | congLib.sml | 201 datatype congset = CS of
208 val empty_congset = CS {cong_reducer=cong_reducer,
216 CS {cong_reducer, relations, dprocs, travrules, limit})
230 CS {cong_reducer=cong_reducer,
260 fun CONGRUENCE_SIMP_QCONV relation (cs as (CS csdata)) ss =
283 fun CONGRUENCE_SIMP_CONV relation (cs as (CS csdata)) ss =
|
| /seL4-l4v-master/seL4/include/arch/x86/arch/machine/ |
| H A D | debug.h | 108 * the CS and SS in the context are set to anything sensible, so
110 setRegister(target_thread, CS, SEL_CS_3);
|
| /seL4-l4v-master/seL4/src/arch/x86/32/ |
| H A D | machine_asm.S | 40 ljmp $0x08, $1f # reload kernel CS with a far jump
|
| H A D | traps.S | 13 #define CS 11 define
19 # Hardware pushes onto the stack SS, ESP, EFLAGS, CS, NextIP and Error,
361 testl $3, (4 * CS)(%esp) # extract CPL (current privilege level)
527 subl $4, %esp # skip CS
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64Script.sml | 234 CS(Var("x",CTy"MXCSR"),
373 CS(Apply
501 CS(Var("index",OTy(PTy(FTy 2,CTy"Zreg"))),
513 CS(Var("base",CTy"Zbase"),
543 CS(Var("rm",CTy"Zrm"),
565 CS(Var("ds",CTy"Zdest_src"),
590 CS(Var("ds",CTy"Zdest_src"),
611 CS(Var("imm_rm",CTy"Zimm_rm"),
624 CS(Var("size",CTy"Zsize"),
632 CS(Va
[all...] |
| /seL4-l4v-master/seL4/src/arch/x86/64/ |
| H A D | c_traps.c | 315 irqstack[2] = getRegister(cur_thread, CS);
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0Script.sml | 153 CS(Var("x",CTy"PRIMASK"),
176 CS(Var("x",CTy"PSR"),
202 CS(Var("x",CTy"CONTROL"),
225 CS(Var("x",CTy"AIRCR"),
253 CS(Var("x",CTy"CCR"),
278 CS(Var("x",CTy"SHPR2"),
300 CS(Var("x",CTy"SHPR3"),
331 CS(Var("x",CTy"IPR"),
356 CS(EX(Var("cond",F4),LN 3,LN 1,FTy 3),
550 CS(nVa
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | Assem.sml | 33 datatype cond = EQ | NE | GE | LE | GT | LT | AL | NV | CC | LS | HI | CS
97 | print_cond (SOME CS) = "CS"
|
| /seL4-l4v-master/HOL4/examples/ARM/v4/ |
| H A D | Data.sml | 5 datatype condition = EQ | NE | CS | CC | MI | PL | VS | VC
|
| H A D | arm_emitScript.sml | 60 if n = 1 then CS else
95 val condition_decl = `condition = EQ | CS | MI | VS | HI | GE | GT | AL |
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/ |
| H A D | riscvScript.sml | 392 CS(Var("a",CTy"Architecture"),
401 CS(Var("ab",FTy 2),
417 CS(Var("a",CTy"Architecture"),
424 CS(Var("p",CTy"Privilege"),
432 CS(Var("p",FTy 2),
440 CS(Var("p",CTy"Privilege"),
450 CS(Var("vm",FTy 5),
471 CS(Var("vm",FTy 5),
477 CS(Var("vm",CTy"VM_Mode"),
489 CS(Va
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
| H A D | arm8Script.sml | 398 CS(Var("x",CTy"TCR_EL1"),
421 CS(Var("x",CTy"TCR_EL2_EL3"),
447 CS(Var("x",CTy"SCTLRType"),
493 CS(Dest("EL",FTy 2,Dest("PSTATE",CTy"ProcState",qVar"state")),
508 CS(Dest
524 CS(Apply(Const("TranslationRegime",ATy(qTy,FTy 2)),qVar"state"),
548 CS(Dest("EL",FTy 2,Dest("PSTATE",CTy"ProcState",qVar"s1")),
666 CS(vVar"l",
771 CS(EX(Var("cond",F4),LN 3,LN 1,FTy 3),
905 CS(Va
[all...] |
| /seL4-l4v-master/HOL4/examples/hardware/hol88/MISC/ |
| H A D | mk_adders.old.ml | 185 CMU-CS-84-101 %
|
| /seL4-l4v-master/HOL4/examples/hardware/hol88/cmos/ |
| H A D | mk_adders.ml | 189 CMU-CS-84-101 %
|